diff --git a/c-refinement/Cogent_Corres.thy b/c-refinement/Cogent_Corres.thy
index 73e4e35d7..f03f0bf0d 100644
--- a/c-refinement/Cogent_Corres.thy
+++ b/c-refinement/Cogent_Corres.thy
@@ -19,6 +19,8 @@ imports
   "../cogent/isa/AssocLookup"
 begin
 
+declare singleton_def[simp]
+
 locale update_sem_init = update_sem +
 constrains abs_typing :: "abstyp \<Rightarrow> name \<Rightarrow> type list \<Rightarrow> sigil \<Rightarrow> ptrtyp set \<Rightarrow> ptrtyp set \<Rightarrow> bool"
        and abs_repr :: "abstyp \<Rightarrow> name \<times> repr list"
@@ -592,6 +594,8 @@ shows "corres srel (Take (Var x) f e) (do z \<leftarrow> gets f'; e' z od) \<xi>
   apply (insert split\<Gamma>)
   apply (erule uval_typing.cases; simp)
   apply (rename_tac \<Xi>' \<sigma>' fs' typ' r1' w1)
+  apply clarsimp
+  thm same_type_as_split_weakened_left
   apply (drule(2) same_type_as_split_weakened_left)
   apply clarsimp
   apply (insert x_unboxed[unfolded corres_def] typing_x)
@@ -944,7 +948,8 @@ proof (clarsimp simp: corres_def in_monad snd_bind snd_modify snd_state_assert,
   have typing_var_elim_lems':
     "[] \<turnstile> \<Gamma>3' \<leadsto>w (Cogent.empty (length \<Gamma>3'))[x := Some (TRecord typ' sgl)]"
     "x < length \<Gamma>3'"
-    using typing_put_elim_lems' by blast+
+    using typing_put_elim_lems' singleton_def
+    by fastforce+
 
   have ftag'_fty'_is:
     "ftag' = fst (typ!f)"
diff --git a/c-refinement/TypeProofGen.thy b/c-refinement/TypeProofGen.thy
index c0746bdd2..25f15d62e 100644
--- a/c-refinement/TypeProofGen.thy
+++ b/c-refinement/TypeProofGen.thy
@@ -125,7 +125,9 @@ fun cleanup_typing_tree_thm ctxt thm =
         t
        )
     |> Simplifier.simplify (put_simpset cleanup_ss ctxt)
-    (* |> Simplifier.simplify ctxt *) (* Hopefully superflous. Didn't cause any changes when run on Bilby *)
+    |> Simplifier.simplify ctxt
+      (* TODO: CorresProof requires the goal to be in a certain shape; cleanup_ss does not
+                put the goals in that shape. Investigate and move the simp rules into cleanup_ss *)
     )
   |> Thm.varifyT_global
 
diff --git a/cogent/isa/Cogent.thy b/cogent/isa/Cogent.thy
index d98bbc9fe..e7fa72240 100644
--- a/cogent/isa/Cogent.thy
+++ b/cogent/isa/Cogent.thy
@@ -533,8 +533,6 @@ definition empty :: "nat \<Rightarrow> ctx" where
 definition singleton :: "nat \<Rightarrow> index \<Rightarrow> type \<Rightarrow> ctx" where
   "singleton n i t \<equiv> (empty n)[i := Some t]"
 
-declare singleton_def [simp]
-
 definition instantiate_ctx :: "type substitution \<Rightarrow> ctx \<Rightarrow> ctx" where
   "instantiate_ctx \<delta> \<Gamma> \<equiv> map (map_option (instantiate \<delta>)) \<Gamma>"
 
@@ -594,6 +592,9 @@ lemmas weakening_cons =  List.list.rel_intros(2)[where R="weakening_comp K" for
 
 lemmas weakening_Cons = list_all2_Cons[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
 
+lemmas weakening_Cons1 = list_all2_Cons1[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
+lemmas weakening_Cons2 = list_all2_Cons2[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
+
 lemmas weakening_conv_all_nth = list_all2_conv_all_nth[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
 
 
@@ -1796,6 +1797,7 @@ lemma instantiate_ctx_singleton [simplified, simp]:
 shows "instantiate_ctx \<delta> (singleton l i \<tau>) = singleton l i (instantiate \<delta> \<tau>)"
 by (induct l arbitrary: i, simp_all add:   instantiate_ctx_def
                                            empty_def
+                                           singleton_def
                                     split: nat.split)
 
 lemma instantiate_ctx_length [simp]:
@@ -2090,7 +2092,7 @@ shows "\<Xi>, K, \<Gamma> \<turnstile>  e  : t  \<Longrightarrow> K \<turnstile>
 and   "\<Xi>, K, \<Gamma> \<turnstile>* es : ts \<Longrightarrow> K \<turnstile>* ts wellformed"
 proof (induct rule: typing_typing_all.inducts)
   case typing_var then show ?case
-    by (fastforce dest: weakening_nth elim: weakening_comp.cases simp add: kinding_defs empty_def)
+    by (fastforce dest: weakening_nth elim: weakening_comp.cases simp add: kinding_defs singleton_def empty_def)
 next case typing_afun then show ?case
     by (clarsimp simp add: kinding_defs instantiate_wellformed list_all2_kinding_wellformedD list_all2_lengthD)
 next case typing_fun then show ?case
diff --git a/cogent/isa/CogentHelper.thy b/cogent/isa/CogentHelper.thy
index c21f8f6ae..12d630f6f 100644
--- a/cogent/isa/CogentHelper.thy
+++ b/cogent/isa/CogentHelper.thy
@@ -15,6 +15,10 @@ theory CogentHelper
 keywords "ML_quiet" :: thy_decl % "ML"
 begin
 
+(* This was in Cogent.thy, but it was removed to make some proofs nicer. Add it here in case
+   the automation depends on it *)
+declare singleton_def[simp]
+
 (* Rewrite rules to get expressions in the assumptions *)
 
 lemma typing_lit': "\<lbrakk> K \<turnstile> \<Gamma> consumed; t = lit_type l \<rbrakk> \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Lit l : TPrim t"
diff --git a/cogent/isa/Correspondence.thy b/cogent/isa/Correspondence.thy
index b3e471f76..a22a48160 100644
--- a/cogent/isa/Correspondence.thy
+++ b/cogent/isa/Correspondence.thy
@@ -128,6 +128,21 @@ and upd_val_rel_record :: "('f \<Rightarrow> poly_type)
                   ; upd.uval_repr_deep x = rp
                   \<rbrakk> \<Longrightarrow> \<Xi>, \<sigma> \<turnstile>* ((x,rp) # xs) \<sim> (x' # xs') :r ((n, t, Taken) # ts) \<langle>r, w\<rangle>"
 
+lemmas upd_val_rel_record_simple_induct =
+  upd_val_rel_upd_val_rel_record.inducts(2)[where ?P1.0=\<open>\<lambda>_ _ _ _ _ _ _. True\<close>, simplified, consumes 1]
+
+inductive_cases u_v_primE     [elim] : "\<Xi>, \<sigma> \<turnstile> UPrim l \<sim> VPrim l' : TPrim \<tau> \<langle>r, w\<rangle>"
+inductive_cases u_v_functionE [elim] : "\<Xi>, \<sigma> \<turnstile> UFunction f ts \<sim> VFunction f' ts' : TFun \<tau> \<rho> \<langle>r, w\<rangle>"
+inductive_cases u_v_afunE     [elim] : "\<Xi>, \<sigma> \<turnstile> UAFunction f ts \<sim> VAFunction f' ts' : TFun \<tau> \<rho> \<langle>r, w\<rangle>"
+inductive_cases u_v_sumE      [elim] : "\<Xi>, \<sigma> \<turnstile> u \<sim> v : TSum \<tau>s \<langle>r, w\<rangle>"
+inductive_cases u_v_productE  [elim] : "\<Xi>, \<sigma> \<turnstile> UProduct a b \<sim> VProduct a' b' : TProduct \<tau> \<rho> \<langle>r, w\<rangle>"
+inductive_cases u_v_recE      [elim] : "\<Xi>, \<sigma> \<turnstile> URecord fs \<sim> VRecord fs' : \<tau> \<langle>r, w\<rangle>"
+inductive_cases u_v_p_recE    [elim] : "\<Xi>, \<sigma> \<turnstile> UPtr p rp \<sim> VRecord fs' : TRecord fs s \<langle>r, w\<rangle>"
+inductive_cases u_v_r_emptyE  [elim] : "\<Xi>, \<sigma> \<turnstile>* [] \<sim> [] :r \<tau>s \<langle>r, w\<rangle>"
+inductive_cases u_v_r_consE   [elim] : "\<Xi>, \<sigma> \<turnstile>* (a # b) \<sim> (a' # b') :r \<tau>s \<langle>r, w\<rangle>"
+inductive_cases u_v_r_consE'  [elim] : "\<Xi>, \<sigma> \<turnstile>* (a # b) \<sim> xx :r \<tau>s \<langle>r, w\<rangle>"
+
+
 lemma upd_val_rel_to_vval_typing:
 shows "\<Xi>, \<sigma> \<turnstile>  u  \<sim> v  :  \<tau>  \<langle>r, w\<rangle> \<Longrightarrow> val.vval_typing \<Xi> v \<tau>"
 and   "\<Xi>, \<sigma> \<turnstile>* us \<sim> vs :r \<tau>s \<langle>r, w\<rangle> \<Longrightarrow> val.vval_typing_record \<Xi> vs \<tau>s"
@@ -164,20 +179,14 @@ next
 qed (auto intro!: upd.uval_typing_uval_typing_record.intros)
 
 
+lemma upd_val_rel_record_length_same:
+  "\<Xi>, \<sigma> \<turnstile>* us \<sim> vs :r ts \<langle>r, w\<rangle> \<Longrightarrow> length us = length ts \<and> length vs = length ts"
+  by (induct rule: upd_val_rel_record_simple_induct) force+
+
+
 lemma u_v_prim' : "\<tau> = lit_type l \<Longrightarrow> l = l' \<Longrightarrow> \<Xi>, \<sigma> \<turnstile> UPrim l \<sim> VPrim l' : TPrim \<tau> \<langle>{}, {}\<rangle>"
    by (simp add: u_v_prim)
 
-inductive_cases u_v_primE     [elim] : "\<Xi>, \<sigma> \<turnstile> UPrim l \<sim> VPrim l' : TPrim \<tau> \<langle>r, w\<rangle>"
-inductive_cases u_v_functionE [elim] : "\<Xi>, \<sigma> \<turnstile> UFunction f ts \<sim> VFunction f' ts' : TFun \<tau> \<rho> \<langle>r, w\<rangle>"
-inductive_cases u_v_afunE     [elim] : "\<Xi>, \<sigma> \<turnstile> UAFunction f ts \<sim> VAFunction f' ts' : TFun \<tau> \<rho> \<langle>r, w\<rangle>"
-inductive_cases u_v_sumE      [elim] : "\<Xi>, \<sigma> \<turnstile> u \<sim> v : TSum \<tau>s \<langle>r, w\<rangle>"
-inductive_cases u_v_productE  [elim] : "\<Xi>, \<sigma> \<turnstile> UProduct a b \<sim> VProduct a' b' : TProduct \<tau> \<rho> \<langle>r, w\<rangle>"
-inductive_cases u_v_recE      [elim] : "\<Xi>, \<sigma> \<turnstile> URecord fs \<sim> VRecord fs' : \<tau> \<langle>r, w\<rangle>"
-inductive_cases u_v_p_recE    [elim] : "\<Xi>, \<sigma> \<turnstile> UPtr p rp \<sim> VRecord fs' : TRecord fs s \<langle>r, w\<rangle>"
-inductive_cases u_v_r_emptyE  [elim] : "\<Xi>, \<sigma> \<turnstile>* [] \<sim> [] :r \<tau>s \<langle>r, w\<rangle>"
-inductive_cases u_v_r_consE   [elim] : "\<Xi>, \<sigma> \<turnstile>* (a # b) \<sim> (a' # b') :r \<tau>s \<langle>r, w\<rangle>"
-inductive_cases u_v_r_consE'  [elim] : "\<Xi>, \<sigma> \<turnstile>* (a # b) \<sim> xx :r \<tau>s \<langle>r, w\<rangle>"
-
 lemma u_v_p_abs_ro': "\<lbrakk> s = Boxed ReadOnly ptrl
                       ; abs_upd_val a a' n ts s r w
                       ; [] \<turnstile>* ts wellformed
@@ -252,6 +261,10 @@ inductive u_v_matches :: "('f \<Rightarrow> poly_type)
 
 inductive_cases u_v_matches_consE: "\<Xi>, \<sigma> \<turnstile> \<gamma> \<sim> \<gamma>' matches (\<tau> # \<tau>s) \<langle> r , w \<rangle>"
 
+lemma u_v_matches_length_same:
+  "\<Xi>, \<sigma> \<turnstile> us \<sim> vs matches \<Gamma> \<langle>r, w\<rangle> \<Longrightarrow> length us = length \<Gamma> \<and> length vs = length \<Gamma>"
+  by (induct rule: u_v_matches.inducts) force+
+
 lemma u_v_matches_to_matches:
 assumes "\<Xi>, \<sigma> \<turnstile> us \<sim> vs matches \<Gamma> \<langle>r, w\<rangle>"
 shows   "val.matches \<Xi> vs \<Gamma>"
@@ -832,29 +845,29 @@ proof -
   from assms obtain env where "singleton (length \<Gamma>) i \<tau> = env" by simp
   from I [simplified this] S assms(3-) this
   show ?thesis proof (induct arbitrary: i \<Gamma> rule: u_v_matches.inducts )
-       case u_v_matches_empty then moreover   have "\<Gamma> = []" by (simp add: empty_def)
+       case u_v_matches_empty then moreover   have "\<Gamma> = []" by (simp add: empty_def singleton_def)
                                     ultimately show ?case    by simp
   next case (u_v_matches_none  \<Xi> \<sigma> xs xs' \<Gamma>' r w x x' i \<Gamma>)
        show ?case proof (cases i)
             case 0       with u_v_matches_none show ?thesis by ( cases "length \<Gamma>"
-                                                               , simp_all add: empty_def )
+                                                               , simp_all add: empty_def singleton_def)
        next case (Suc n)
          moreover with u_v_matches_none have "\<Gamma>' = (empty (length \<Gamma> - 1))[n := Some \<tau>]"
-                                         by (cases "length \<Gamma>", simp_all add: empty_def)
+                                         by (cases "length \<Gamma>", simp_all add: empty_def singleton_def)
          moreover with u_v_matches_none have "length \<Gamma> = Suc (length \<Gamma>')"
-                                         by (simp add: empty_def)
+                                         by (simp add: empty_def singleton_def)
          ultimately show ?thesis apply -
                                  apply (insert u_v_matches_none)
-                                 apply (auto).
+                                 apply (auto simp add: singleton_def).
        qed
   next case (u_v_matches_some)
        show ?case proof (cases i)
             case 0 with u_v_matches_some show ?thesis
-              apply (cases "length \<Gamma>", simp_all add: empty_def)
+              apply (cases "length \<Gamma>", simp_all add: empty_def singleton_def)
               apply (clarsimp dest!:u_v_matches_empty_env(2) [simplified empty_def])
               apply (blast).
        next case (Suc n) with u_v_matches_some show ?thesis by ( cases "length \<Gamma>"
-                                                                , simp_all add: empty_def )
+                                                                , simp_all add: empty_def singleton_def)
        qed
   qed
 qed
@@ -1243,7 +1256,6 @@ lemma value_subtyping:
     and "\<Xi>, \<sigma> \<turnstile>* vs \<sim> vs' :r ts \<langle>r, w\<rangle>
           \<Longrightarrow> [] \<turnstile> TRecord ts s \<sqsubseteq> TRecord ts' s
           \<Longrightarrow> \<exists>r'. r' \<subseteq> r \<and> \<Xi>, \<sigma> \<turnstile>* vs \<sim> vs' :r ts' \<langle>r', w\<rangle>"
-(* TODO clean up and rewrite as Isar proof *)
 proof (induct arbitrary: t' and ts' s rule: upd_val_rel_upd_val_rel_record.inducts)
   case (u_v_product \<Xi> \<sigma> a a' t r w b b' u r' w')
   then show ?case
@@ -1323,7 +1335,7 @@ next
     apply -
     apply (erule subtyping.cases; clarsimp)
     apply (rule_tac V="[] \<turnstile> TRecord ts (Boxed ReadOnly ptrl) \<sqsubseteq> TRecord ts2 (Boxed ReadOnly ptrl)" in revcut_rl)
-     using u_v_p_rec_ro.prems apply blast
+    apply (fast intro!: subtyping.intros)
     apply (rule_tac V="\<exists>r'\<subseteq>r. \<Xi>, \<sigma> \<turnstile>* fs \<sim> fs' :r ts2 \<langle>r', {}\<rangle>" in revcut_rl, blast)
     apply (erule exE)
     apply (erule conjE)
@@ -1338,7 +1350,7 @@ next
     apply -
     apply (erule subtyping.cases; clarsimp)
     apply (rule_tac V="[] \<turnstile> TRecord ts (Boxed Writable ptrl) \<sqsubseteq> TRecord ts2 (Boxed Writable ptrl)" in revcut_rl)
-     using u_v_p_rec_w.prems apply blast
+    apply (fast intro!: subtyping.intros)
     apply (rule_tac V="\<exists>r'\<subseteq>r. \<Xi>, \<sigma> \<turnstile>* fs \<sim> fs' :r ts2 \<langle>r', w\<rangle>" in revcut_rl, blast)
     apply (erule exE)
     apply (erule conjE)
@@ -1373,17 +1385,16 @@ next
     apply (elim exE)
     apply (elim conjE)
     apply (case_tac b; simp)
-     apply (rule_tac V="w = {}" in revcut_rl)
-      using u_v_discardable_not_writable(1) apply fastforce
-     apply (rule_tac x="r'aa" in exI)
-     apply (intro conjI, blast)
-     apply (intro upd_val_rel_upd_val_rel_record.intros)
-         apply simp
-        apply (metis kinding_to_wellformedD(1) record_state.distinct(1) snd_conv subtyping_wellformed_preservation(1))
-       apply (simp add: subtyping_preserves_type_repr)
-      apply (metis subtyping_preserves_type_repr upd.type_repr_uval_repr(1) upd_val_rel_to_uval_typing(1))
-     apply (metis subtyping_preserves_type_repr upd.type_repr_uval_repr_deep(1) upd_val_rel_to_uval_typing(1))
-
+     apply (subgoal_tac "w = {}")
+      apply (rule_tac x="r'aa" in exI)
+      apply (intro conjI, blast)
+      apply (intro upd_val_rel_upd_val_rel_record.intros)
+          apply simp
+         apply (metis kinding_to_wellformedD(1) record_state.distinct(1) snd_conv subtyping_wellformed_preservation(1))
+        apply (simp add: subtyping_preserves_type_repr)
+       apply (metis subtyping_preserves_type_repr upd.type_repr_uval_repr(1) upd_val_rel_to_uval_typing(1))
+      apply (metis subtyping_preserves_type_repr upd.type_repr_uval_repr_deep(1) upd_val_rel_to_uval_typing(1))
+    apply (meson singletonI u_v_discardable_not_writable(1))
     apply (rule_tac x="r'a \<union> r'aa" in exI)
     apply (intro conjI, blast)
     apply (intro upd_val_rel_upd_val_rel_record.intros; (simp add: subtyping_preserves_type_repr)?; blast?)
@@ -1399,8 +1410,8 @@ next
     apply (rule_tac x="r'" in exI)
     apply (intro conjI, blast)
     apply (case_tac b; clarsimp)
-    using subtyping_wellformed_preservation(1)
     apply (fastforce
+        dest: subtyping_wellformed_preservation
         intro!: upd_val_rel_upd_val_rel_record.intros
         simp add: subtyping_preserves_type_repr)
     done
@@ -2259,6 +2270,9 @@ and     "\<lbrakk> \<xi> , \<gamma>  \<turnstile>* (\<sigma>, es) \<Down>! (\<si
   using assms proof (induct "(\<sigma>,e)" "(\<sigma>',v)"
     and "(\<sigma>,es)" "(\<sigma>', vs)" arbitrary: \<Gamma> r w \<sigma> e v \<tau> \<sigma>' \<gamma>' and \<Gamma> r w  \<sigma> es vs \<tau>s' \<sigma>'  \<gamma>'
     rule: u_sem_u_sem_all.inducts)
+  case u_sem_var then show ?case
+    by (force dest: u_v_matches_length_same intro: v_sem_v_sem_all.intros)
+next
      case u_sem_cast
   note IH   = this(2)
   and  rest = this(1,3-)
@@ -2317,15 +2331,19 @@ next case (u_sem_abs_app _ _ _ _ _ f)
     apply (rule,erule(2) v_sem_abs_app)
     done
 next case u_sem_con then show ?case by (force intro!: v_sem_v_sem_all.intros)
-next case u_sem_member
+next case (u_sem_member \<xi> \<gamma> \<sigma> e \<sigma>' fs f)
   note IH = this(2)
   and rest = this(1,3-)
   from rest show ?case
-    apply (clarsimp elim!: typing_memberE)
+    apply -
+    apply (erule typing_memberE)
     apply (frule(3) IH, clarsimp)
     apply (frule(5) mono_correspondence, clarsimp)
-    apply (force elim: upd_val_rel.cases intro!: v_sem_v_sem_all.intros)
-  done
+    apply (force
+        intro!: v_sem_v_sem_all.intros
+        dest: upd_val_rel_record_length_same
+        elim: upd_val_rel.cases)
+    done
 next case u_sem_memb_b
   note IH = this(2)
   and rest = this(1,3-)
@@ -2333,7 +2351,10 @@ next case u_sem_memb_b
     apply (clarsimp elim!: typing_memberE)
     apply (frule(3) IH, clarsimp)
     apply (frule(5) mono_correspondence, clarsimp)
-    apply (force elim: upd_val_rel.cases intro!: v_sem_v_sem_all.intros)
+    apply (force
+        intro!: v_sem_v_sem_all.intros
+        dest: upd_val_rel_record_length_same
+        elim: upd_val_rel.cases)
   done
 next case u_sem_esac
   note IH = this(2)
@@ -2593,8 +2614,13 @@ next case u_sem_take
        apply (blast)
       apply (blast)
      apply (blast)
-    apply (force intro: v_sem_v_sem_all.intros)
-  done
+    apply (frule upd_val_rel_record_length_same; clarsimp)
+    apply (rule exI)
+    apply (rule v_sem_v_sem_all.intros)
+      apply blast
+     apply blast
+    apply argo
+    done
 next case u_sem_take_ub
   note IH1 = this(2)
   and  IH2 = this(4)
@@ -2647,7 +2673,12 @@ next case u_sem_take_ub
        apply (blast)
       apply (blast)
      apply (blast)
-    apply (force intro: v_sem_v_sem_all.intros)
+    apply (frule upd_val_rel_record_length_same; clarsimp)
+    apply (rule exI)
+    apply (rule v_sem_v_sem_all.intros)
+      apply blast
+     apply blast
+    apply argo
   done
 next case u_sem_put
   note IH1 = this(2)
@@ -2661,7 +2692,12 @@ next case u_sem_put
     apply (drule(5) mono_correspondence [rotated -1], clarsimp)
     apply (frule(5) IH2 [OF _ _ u_v_matches_frame,rotated -1],force)
     apply (erule upd_val_rel.cases,simp_all)
-    apply (force intro: v_sem_v_sem_all.intros)
+    apply (frule upd_val_rel_record_length_same; clarsimp)
+    apply (rule exI)
+    apply (rule v_sem_v_sem_all.intros)
+      apply blast
+     apply blast
+    apply argo
   done
 next case u_sem_put_ub
   note IH1 = this(2)
@@ -2675,7 +2711,12 @@ next case u_sem_put_ub
     apply (drule(5) mono_correspondence [rotated -1], clarsimp)
     apply (frule(5) IH2 [OF _ _ u_v_matches_frame,rotated -1],force)
     apply (erule upd_val_rel.cases,simp_all)
-    apply (force intro: v_sem_v_sem_all.intros)
+    apply (frule upd_val_rel_record_length_same; clarsimp)
+    apply (rule exI)
+    apply (rule v_sem_v_sem_all.intros)
+      apply blast
+     apply blast
+    apply argo
     done
 next
   case (u_sem_promote \<xi> \<gamma> \<sigma> e t')
diff --git a/cogent/isa/Subtyping.thy b/cogent/isa/Subtyping.thy
index 243225f2e..08f1d78c0 100644
--- a/cogent/isa/Subtyping.thy
+++ b/cogent/isa/Subtyping.thy
@@ -1,5 +1,7 @@
 theory Subtyping
-  imports Cogent
+  imports
+    Cogent
+    ValueSemantics
 begin
 
 text \<open>
@@ -8,6 +10,8 @@ text \<open>
   the correct relation.
 \<close>
 
+section \<open>Subtyping As An Order and As A Lattice\<close>
+
 inductive type_lub :: "kind env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ \<leftarrow> _ \<squnion> _" [60,0,0,60] 60)
   and type_glb :: "kind env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ \<leftarrow> _ \<sqinter> _" [60,0,0,60] 60)
   where
@@ -270,7 +274,8 @@ next
       "K \<turnstile> TSum ts1 wellformed"
       "K \<turnstile> TSum ts2 wellformed"
       using lub_tsum.hyps type_lub_type_glb_wellformed_produce_wellformed
-      by (metis (mono_tags, lifting) list_all3_conv_all_nth list_all_length type_wellformed.simps(6) type_wellformed_pretty_def)+
+      by (metis (mono_tags, lifting) list_all3_conv_all_nth list_all_length 
+                type_wellformed.simps(6) type_wellformed_pretty_def)+
     have "K \<turnstile> TSum ts1 :\<kappa> {D}"
       using lub_tsum
     proof (clarsimp simp: kinding_variant_conv_all_nth kinding_simps)
@@ -531,4 +536,177 @@ theorem type_glb_type_lub_subtyping_equivalent:
     "K \<turnstile> b \<leftarrow> a \<sqinter> b \<longleftrightarrow> K \<turnstile> b \<sqsubseteq> a"
   using subtyping_to_type_lub type_lub_type_glb_to_subtyping subtyping_to_type_glb by blast+
 
+lemmas weakening_append1 = list_all2_append1[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
+lemmas weakening_append2 = list_all2_append2[where P="weakening_comp K" for K, simplified weakening_def[symmetric]]
+
+lemma take_empty:
+  assumes \<open>m < n\<close>
+  shows \<open>take m (empty n) = empty m\<close>
+  unfolding empty_def
+  using assms by auto
+
+lemma drop_empty:
+  assumes \<open>m < n\<close>
+  shows \<open>drop m (empty n) = empty (n - m)\<close>
+  unfolding empty_def
+  using assms by auto
+
+lemma weaken_to_singleton_split:
+  assumes
+    \<open>i < length \<Gamma>\<close>
+  shows
+    \<open>(K \<turnstile> \<Gamma> \<leadsto>w (singleton (length \<Gamma>) i t))
+     \<longleftrightarrow>
+     (\<exists>\<Gamma>a \<Gamma>b.
+       \<Gamma> = \<Gamma>a @ [\<Gamma> ! i] @ \<Gamma>b \<and>
+       (K \<turnstile> \<Gamma>a \<leadsto>w empty i) \<and>
+       weakening_comp K (\<Gamma> ! i) (Some t) \<and>
+       (K \<turnstile> \<Gamma>b \<leadsto>w empty (length \<Gamma> - Suc i)))\<close>
+  using assms
+  apply (clarsimp simp add:
+      singleton_def upd_conv_take_nth_drop empty_length
+      weakening_append2 weakening_Cons2 min_absorb2 take_empty drop_empty)
+  apply safe
+   apply (metis Cogent.empty_def drop_replicate nth_append_length)
+  apply (metis (mono_tags, lifting) Cogent.empty_def drop_replicate empty_length length_Cons weakening_length)
+  done
+
+section \<open>Subtyping and Value Semantics\<close>
+
+fun strip_promote :: \<open>'f expr \<Rightarrow> 'f expr\<close> where
+  \<open>strip_promote (Var i) = (Var i)\<close>
+| \<open>strip_promote (AFun n ts) = (AFun n ts)\<close>
+| \<open>strip_promote (Fun e ts) = (Fun (strip_promote e) ts)\<close>
+| \<open>strip_promote (Prim p es) = (Prim p (map strip_promote es))\<close>
+| \<open>strip_promote (App ef ea) = (App (strip_promote ef) (strip_promote ea))\<close>
+| \<open>strip_promote (Con vs n e) = (Con vs n (strip_promote e))\<close>
+| \<open>strip_promote (Struct fs es) = (Struct fs (map strip_promote es))\<close>
+| \<open>strip_promote (Member e n) = (Member (strip_promote e) n)\<close>
+| \<open>strip_promote Unit = Unit\<close>
+| \<open>strip_promote (Lit l) = Lit l\<close>
+| \<open>strip_promote (SLit s) = SLit s\<close>
+| \<open>strip_promote (Cast m e) = (Cast m (strip_promote e))\<close>
+| \<open>strip_promote (Tuple ea eb) = (Tuple (strip_promote ea) (strip_promote eb))\<close>
+| \<open>strip_promote (Put er n ec) = (Put (strip_promote er) n (strip_promote ec))\<close>
+| \<open>strip_promote (Let ea ec) = (Let (strip_promote ea) (strip_promote ec))\<close>
+| \<open>strip_promote (LetBang is ea ec) = (LetBang is (strip_promote ea) (strip_promote ec))\<close>
+| \<open>strip_promote (Case ev n ecm ecnm) = (Case (strip_promote ev) n (strip_promote ecm) (strip_promote ecnm))\<close>
+| \<open>strip_promote (Esac ec n) = (Esac (strip_promote ec) n)\<close>
+| \<open>strip_promote (If ec et ef) = (If (strip_promote ec) (strip_promote et) (strip_promote ef))\<close>
+| \<open>strip_promote (Take er n ec) = (Take (strip_promote er) n (strip_promote ec))\<close>
+| \<open>strip_promote (Split et ec) = (Split (strip_promote et) (strip_promote ec))\<close>
+| \<open>strip_promote (Promote type e) = strip_promote e\<close>
+
+
+fun strip_promote_val :: \<open>('a, 'b) vval \<Rightarrow> ('a, 'b) vval\<close> where
+  \<open>strip_promote_val (VPrim l) = VPrim l\<close>
+| \<open>strip_promote_val (VProduct v1 v2) = VProduct (strip_promote_val v1) (strip_promote_val v2)\<close>
+| \<open>strip_promote_val (VSum n v) = VSum n (strip_promote_val v)\<close>
+| \<open>strip_promote_val (VRecord vs) = VRecord (map strip_promote_val vs)\<close>
+| \<open>strip_promote_val (VAbstract a) = (VAbstract a)\<close>
+| \<open>strip_promote_val (VFunction f ts) = VFunction (strip_promote f) ts\<close>
+| \<open>strip_promote_val (VAFunction n ts) = VAFunction n ts\<close>
+| \<open>strip_promote_val VUnit = VUnit\<close>
+
+lemma typing_promote_idem:
+  "\<Xi>, K, \<Gamma> \<turnstile> e' : t \<Longrightarrow> e' = Promote t1 (Promote t2 e) \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Promote t1 e : t"
+  "\<Xi>, K, \<Gamma> \<turnstile>* es : ts \<Longrightarrow> True"
+  using subtyping_trans typing_promote
+  by (induct arbitrary: t1 t2 e rule: typing_typing_all.inducts) blast+
+
+context value_sem
+begin
+
+lemma strip_promote_val_eval_prim:
+  shows "strip_promote_val (eval_prim p vs) = eval_prim p (map strip_promote_val vs)"
+  unfolding eval_prim_def
+  apply clarsimp
+  apply (rule_tac f=\<open>\<lambda>f. eval_prim_op p (map f vs)\<close> in cong, simp)
+  apply (rule ext)
+  apply (rename_tac v)
+  apply (case_tac v; clarsimp)
+  done
+
+lemma specialise_strip_promote_eq_stip_promote_specialise:
+  shows "specialise ts (strip_promote e) = strip_promote (specialise ts e)"
+  by (induct e; clarsimp)
+
+lemma strip_promote_eval_same: 
+    \<open>\<xi> , \<gamma> \<turnstile> e \<Down> v \<Longrightarrow>
+      (\<And>f a r. \<xi> f a r \<Longrightarrow> \<xi> f (strip_promote_val a) (strip_promote_val r)) \<Longrightarrow>
+     \<xi> , map strip_promote_val \<gamma> \<turnstile> strip_promote e \<Down> strip_promote_val v\<close>
+    \<open>\<xi> , \<gamma> \<turnstile>* es \<Down> vs \<Longrightarrow>
+     (\<And>f a r. \<xi> f a r \<Longrightarrow> \<xi> f (strip_promote_val a) (strip_promote_val r)) \<Longrightarrow>
+     \<xi> , map strip_promote_val \<gamma> \<turnstile>* map strip_promote es \<Down> map strip_promote_val vs\<close>
+proof (induct rule: v_sem_v_sem_all.inducts)
+  case (v_sem_var i \<gamma> \<xi>)
+  then show ?case 
+    by (simp add: v_sem_var_mapped_ctx)
+next
+  case (v_sem_prim \<xi> \<gamma> as as' p)
+  then show ?case 
+    by (simp add: strip_promote_val_eval_prim v_sem_v_sem_all.v_sem_prim)
+next
+  case (v_sem_app \<xi> \<gamma> x e ts y a r)
+  then show ?case 
+    by (fastforce 
+        simp: specialise_strip_promote_eq_stip_promote_specialise 
+        intro!:v_sem_v_sem_all.v_sem_app) 
+next
+  case (v_sem_member f fs \<xi> \<gamma> e)
+  then show ?case 
+    by (simp add: v_sem_member_mapped_fields) 
+next
+  case (v_sem_if \<xi> \<gamma> x b t e r)
+  then show ?case 
+    by (fastforce intro!:v_sem_v_sem_all.intros)
+next
+  case (v_sem_put \<xi> \<gamma> x fs e e' f)
+  then show ?case 
+    by (simp add: map_update v_sem_v_sem_all.v_sem_put)
+qed (simp_all add: v_sem_v_sem_all.intros)
+
+lemma val_eval_deterministic:
+  assumes "\<And>f a r r'. \<xi> f a r \<Longrightarrow> \<xi> f a r' \<Longrightarrow> r = r'"
+  shows   "\<xi>, \<gamma> \<turnstile> e \<Down> v \<Longrightarrow> \<xi>, \<gamma> \<turnstile> e \<Down> v' \<Longrightarrow> v' = v"
+  and     "\<xi>, \<gamma> \<turnstile>* es \<Down> vs \<Longrightarrow>  \<xi>, \<gamma> \<turnstile>* es \<Down> vs' \<Longrightarrow> vs' = vs"
+  using assms
+proof (induct arbitrary: v' and vs' rule: v_sem_v_sem_all.inducts)
+  case (v_sem_cast \<xi> \<gamma> e l \<tau> l')
+  then show ?case by fastforce
+next
+  case (v_sem_case_nm \<xi> \<gamma> x t' v t n n' m)
+  then show ?case 
+    by (blast elim!: v_sem_caseE) 
+qed blast+
+
+
+lemma coherence_of_subsumption:
+  assumes  
+     \<open> \<xi> , \<gamma> \<turnstile> e \<Down> v \<close>
+     \<open> \<xi> , \<gamma> \<turnstile> e' \<Down> v' \<close>
+     \<open> strip_promote e' = strip_promote e \<close>
+     \<open> \<And>f a r. \<xi> f a r \<Longrightarrow> \<xi> f (strip_promote_val a) (strip_promote_val r) \<close>
+     \<open> \<And>f a r r'. \<xi> f a r\<Longrightarrow> \<xi> f a r'  \<Longrightarrow> r = r' \<close>
+   shows  \<open> strip_promote_val v = strip_promote_val v' \<close>
+  apply (insert assms)
+  apply (drule strip_promote_eval_same(1), simp)
+  apply (drule strip_promote_eval_same(1), simp)
+  by (rule val_eval_deterministic[where \<xi> = \<xi>], simp_all)  
+
+lemma coherence_of_subsumption_list:
+  assumes  
+     \<open> \<xi> , \<gamma> \<turnstile>* es \<Down> vs \<close>
+     \<open> \<xi> , \<gamma> \<turnstile>* es' \<Down> vs' \<close>
+     \<open> map strip_promote es' = map strip_promote es \<close>
+     \<open> \<And>f a r. \<xi> f a r \<Longrightarrow> \<xi> f (strip_promote_val a) (strip_promote_val r) \<close>
+     \<open> \<And>f a r r'. \<xi> f a r\<Longrightarrow> \<xi> f a r'  \<Longrightarrow> r = r' \<close>
+   shows  \<open> map strip_promote_val vs = map strip_promote_val vs' \<close>
+  apply (insert assms)
+  apply (drule strip_promote_eval_same(2), simp)
+  apply (drule strip_promote_eval_same(2), simp)
+  by (rule val_eval_deterministic[where \<xi> = \<xi>], simp_all)
+
+end
+
 end
\ No newline at end of file
diff --git a/cogent/isa/TypeTrackingSemantics.thy b/cogent/isa/TypeTrackingSemantics.thy
index 7ca30d00a..159938cea 100644
--- a/cogent/isa/TypeTrackingSemantics.thy
+++ b/cogent/isa/TypeTrackingSemantics.thy
@@ -608,8 +608,8 @@ next
         intro: u_sem_var[where \<gamma>="x # xs" and i=0 for x xs, simplified]
         dest: u_tt_sem_pres_type_wellformed2
         simp add: composite_anormal_expr_def empty_def weakening_def weakening_comp.simps
-        list_all2_same kinding_iff_wellformed)
-    apply (frule u_tt_sem_pres_preservation, (simp+)[3])
+                  singleton_def list_all2_same kinding_iff_wellformed)
+     apply (frule u_tt_sem_pres_preservation, (simp+)[3])
     apply (force dest: u_tt_sem_pres_length intro: matches_ptrs_some matches_ptrs_replicate_None)
     done
 next
diff --git a/cogent/isa/UpdateSemantics.thy b/cogent/isa/UpdateSemantics.thy
index f9ba69cb1..3190fd8c6 100644
--- a/cogent/isa/UpdateSemantics.thy
+++ b/cogent/isa/UpdateSemantics.thy
@@ -970,29 +970,29 @@ proof -
   from assms obtain env where "singleton (length \<Gamma>) i \<tau> = env" by simp
   from I [simplified this] S assms(3-) this
   show ?thesis proof (induct arbitrary: i \<Gamma> rule: matches_ptrs.inducts )
-       case matches_ptrs_empty then moreover   have "\<Gamma> = []" by (simp add: empty_def)
+       case matches_ptrs_empty then moreover   have "\<Gamma> = []" by (simp add: empty_def singleton_def)
                                     ultimately show ?case    by simp
   next case (matches_ptrs_none  \<Xi> \<sigma> xs \<Gamma>' r w x i \<Gamma>)
        show ?case proof (cases i)
             case 0       with matches_ptrs_none show ?thesis by ( cases "length \<Gamma>"
-                                                                , simp_all add: empty_def )
+                                                                , simp_all add: empty_def singleton_def)
        next case (Suc n)
          moreover with matches_ptrs_none have "\<Gamma>' = (empty (length \<Gamma> - 1))[n := Some \<tau>]"
-                                         by (cases "length \<Gamma>", simp_all add: empty_def)
+                                         by (cases "length \<Gamma>", simp_all add: empty_def singleton_def)
          moreover with matches_ptrs_none have "length \<Gamma> = Suc (length \<Gamma>')"
-                                         by (simp add: empty_def)
+                                         by (simp add: empty_def singleton_def)
          ultimately show ?thesis apply -
                                  apply (insert matches_ptrs_none)
-                                 apply (auto).
+                                 apply (auto simp add: singleton_def) .
        qed
   next case (matches_ptrs_some)
        show ?case proof (cases i)
             case 0 with matches_ptrs_some show ?thesis
-              apply (cases "length \<Gamma>", simp_all add: empty_def)
-              apply (clarsimp dest!:matches_ptrs_empty_env(2) [simplified empty_def])
+              apply (cases "length \<Gamma>", simp_all add: empty_def singleton_def)
+              apply (clarsimp dest!:matches_ptrs_empty_env(2)[simplified empty_def])
               apply (blast).
        next case (Suc n) with matches_ptrs_some show ?thesis by ( cases "length \<Gamma>"
-                                                                , simp_all add: empty_def )
+                                                                , simp_all add: empty_def singleton_def)
        qed
   qed
 qed
diff --git a/cogent/isa/ValueSemantics.thy b/cogent/isa/ValueSemantics.thy
index c3fa34b2a..58979a345 100644
--- a/cogent/isa/ValueSemantics.thy
+++ b/cogent/isa/ValueSemantics.thy
@@ -55,7 +55,7 @@ inductive v_sem :: "('f,'a) vabsfuns \<Rightarrow> ('f, 'a) vval env \<Rightarro
 and       v_sem_all  :: "('f,'a) vabsfuns \<Rightarrow> ('f, 'a) vval list \<Rightarrow> 'f expr list \<Rightarrow> ('f, 'a) vval list \<Rightarrow> bool"
           ("_ , _ \<turnstile>* _ \<Down> _" [30,0,0,20] 60)
 where
-  v_sem_var     : "\<xi> , \<gamma> \<turnstile> (Var i) \<Down> (\<gamma> ! i)"
+  v_sem_var     : "i < length \<gamma> \<Longrightarrow> \<xi> , \<gamma> \<turnstile> (Var i) \<Down> (\<gamma> ! i)"
 
 | v_sem_lit     : "\<xi> , \<gamma> \<turnstile> (Lit l) \<Down> VPrim l"
 
@@ -84,6 +84,7 @@ where
                    \<rbrakk> \<Longrightarrow> \<xi> , \<gamma> \<turnstile> (Con _ t x) \<Down> VSum t x'"
 
 | v_sem_member  : "\<lbrakk> \<xi> , \<gamma> \<turnstile> e \<Down> VRecord fs
+                   ; f < length fs
                    \<rbrakk> \<Longrightarrow> \<xi> , \<gamma> \<turnstile> Member e f \<Down> fs ! f"
 
 | v_sem_unit    : "\<xi> , \<gamma> \<turnstile> Unit \<Down> VUnit"
@@ -121,10 +122,12 @@ where
 
 | v_sem_take    : "\<lbrakk> \<xi> , \<gamma> \<turnstile> x \<Down> VRecord fs
                    ; \<xi> , (fs ! f # VRecord fs # \<gamma>) \<turnstile> e \<Down> e'
+                   ; f < length fs
                    \<rbrakk> \<Longrightarrow> \<xi> , \<gamma> \<turnstile> Take x f e \<Down> e'"
 
 | v_sem_put     : "\<lbrakk> \<xi> , \<gamma> \<turnstile> x \<Down> VRecord fs
                    ; \<xi> , \<gamma> \<turnstile> e \<Down> e'
+                   ; f < length fs
                    \<rbrakk> \<Longrightarrow> \<xi> , \<gamma> \<turnstile> Put x f e \<Down> VRecord (fs [ f := e' ])"
 
 | v_sem_split   : "\<lbrakk> \<xi> , \<gamma> \<turnstile> x \<Down> VProduct a b
@@ -141,11 +144,37 @@ where
                      ; \<xi> , \<gamma> \<turnstile>* xs \<Down> vs
                      \<rbrakk> \<Longrightarrow> \<xi> , \<gamma> \<turnstile>* (x # xs) \<Down> (v # vs)"
 
-inductive_cases v_sem_varE  [elim] : "\<xi> , \<gamma> \<turnstile> Var i \<Down> v"
-inductive_cases v_sem_funE  [elim] : "\<xi> , \<gamma> \<turnstile> Fun f ts \<Down> v"
-inductive_cases v_sem_afunE [elim] : "\<xi> , \<gamma> \<turnstile> AFun f ts \<Down> v"
-inductive_cases v_sem_appE  [elim] : "\<xi> , \<gamma> \<turnstile> App a b \<Down> v"
-
+inductive_cases v_sem_varE    [elim] : "\<xi> , \<gamma> \<turnstile> Var i \<Down> v"
+inductive_cases v_sem_litE    [elim] : "\<xi> , \<gamma> \<turnstile> Lit l \<Down> v"
+inductive_cases v_sem_primE   [elim] : "\<xi> , \<gamma> \<turnstile> Prim p as \<Down> v"
+inductive_cases v_sem_funE    [elim] : "\<xi> , \<gamma> \<turnstile> Fun f ts \<Down> v"
+inductive_cases v_sem_afunE   [elim] : "\<xi> , \<gamma> \<turnstile> AFun f ts \<Down> v"
+inductive_cases v_sem_appE    [elim] : "\<xi> , \<gamma> \<turnstile> App a b \<Down> v"
+inductive_cases v_sem_castE   [elim]: " \<xi> , \<gamma> \<turnstile> Cast \<tau> e \<Down> v"
+inductive_cases v_sem_conE    [elim]: " \<xi> , \<gamma> \<turnstile> Con l t x \<Down> v"
+inductive_cases v_sem_memberE [elim]: " \<xi> , \<gamma> \<turnstile> Member e f \<Down> v"
+inductive_cases v_sem_unitE   [elim]: " \<xi> , \<gamma> \<turnstile> Unit \<Down> v"
+inductive_cases v_sem_tupleE  [elim]: " \<xi> , \<gamma> \<turnstile> Tuple x y \<Down> v"
+inductive_cases v_sem_esacE   [elim]: " \<xi> , \<gamma> \<turnstile> Esac t ts \<Down> v"
+inductive_cases v_sem_letE    [elim]: " \<xi> , \<gamma> \<turnstile> Let a b \<Down> v"
+inductive_cases v_sem_letbangE[elim]: " \<xi> , \<gamma> \<turnstile> LetBang vs a b \<Down> v"
+inductive_cases v_sem_caseE   [elim]: " \<xi> , \<gamma> \<turnstile> Case x t m n \<Down> v"
+inductive_cases v_sem_ifE     [elim]: " \<xi> , \<gamma> \<turnstile> If x t e \<Down> v"
+inductive_cases v_sem_structE [elim]: " \<xi> , \<gamma> \<turnstile> Struct ts xs \<Down> v"
+inductive_cases v_sem_takeE   [elim]: " \<xi> , \<gamma> \<turnstile> Take x f e \<Down> v"
+inductive_cases v_sem_putE    [elim]: " \<xi> , \<gamma> \<turnstile> Put x f e \<Down> v"
+inductive_cases v_sem_splitE  [elim]: " \<xi> , \<gamma> \<turnstile> Split x e \<Down> v"
+inductive_cases v_sem_promoteE[elim] : "\<xi> , \<gamma> \<turnstile> Promote t e \<Down> v"
+inductive_cases v_sem_emptyE  [elim]: " \<xi> , \<gamma> \<turnstile>* [] \<Down> v"
+inductive_cases v_sem_consE   [elim]: " \<xi> , \<gamma> \<turnstile>* x # xs \<Down> v"
+
+lemma v_sem_var_mapped_ctx:
+  shows "i < length \<gamma> \<Longrightarrow> \<xi>' , map f \<gamma> \<turnstile> Var i \<Down> f (\<gamma> ! i)"
+  by (metis length_map nth_map v_sem_var)
+
+lemma v_sem_member_mapped_fields:
+  shows "f < length fs \<Longrightarrow> \<xi> , \<gamma> \<turnstile> e \<Down> VRecord (map g fs) \<Longrightarrow> \<xi> , \<gamma> \<turnstile> Member e f \<Down> g (fs ! f)"
+  by (metis length_map nth_map v_sem_member)
 
 locale value_sem =
   fixes abs_typing :: "'a \<Rightarrow> name \<Rightarrow> type list \<Rightarrow> bool"
@@ -812,7 +841,7 @@ using assms proof (induct "specialise \<tau>s e"        v
      case v_sem_var     then show ?case by ( case_tac e, simp_all
                                            , fastforce dest:  matches_weakening
                                                        intro: matches_proj
-                                                       simp:  empty_length empty_def)
+                                                       simp:  empty_length empty_def singleton_def)
 next case v_sem_lit     then show ?case by ( case_tac e, simp_all
                                            , fastforce intro: vval_typing_vval_typing_record.intros)
 next case v_sem_prim    then show ?case by ( case_tac e, simp_all
@@ -960,7 +989,7 @@ next
       "spec_x = specialise \<tau>s x"
       "f' = f"
       "spec_y = specialise \<tau>s y"
-      using v_sem_take(5) Take by simp+
+      using v_sem_take.hyps Take by simp+
     
     obtain \<Gamma>1 \<Gamma>2 ts s n t k taken
       where typing_elims:
@@ -1233,7 +1262,7 @@ then show ?case
   apply (rule v_sem_v_sem_all.v_sem_abs_app, erule(5) IH1 [OF _ _ _ matches_split'(1), simplified], erule(5) IH2 [OF _ _ _ matches_split'(2), simplified])
   apply (simp add: monoprog_def)
 done
-next case v_sem_var then show ?case by (simp, metis matches_length nth_map typing_varE v_sem_v_sem_all.v_sem_var)
+next case v_sem_var then show ?case by (fastforce intro: v_sem_var_mapped_ctx)
 next case v_sem_lit then show ?case by (fastforce intro!: v_sem_v_sem_all.v_sem_lit)
 next case v_sem_fun then show ?case by (fastforce intro!: v_sem_v_sem_all.v_sem_fun)
 next case v_sem_afun then show ?case by (fastforce intro!: v_sem_v_sem_all.v_sem_afun)
@@ -1297,11 +1326,7 @@ from rest show ?case
                 elim: v_t_productE)
 done
 next case v_sem_member then show ?case
-  apply (clarsimp elim!: typing_memberE)
-  apply (subst member_nth_map
-        , (force dest:preservation [where \<tau>s = "[]" and K = "[]", simplified] elim!: v_t_recordE dest: vval_typing_record_length intro: v_sem_v_sem_all.intros)+
-        )
-done
+    by (force intro: v_sem_member_mapped_fields elim!: typing_memberE)
 next case v_sem_prim
 note IH = this(2)
 and rest = this(1,3-)