Changeset 2438 for src/Clight/switchRemoval.ma

Timestamp:

Nov 7, 2012, 11:18:56 AM (7 years ago)

Author:

garnier

Message:

Sync of the w.i.p. for switch removal.

File:

• src/Clight/switchRemoval.ma (modified) (43 diffs)

src/Clight/switchRemoval.ma

@@ -9 +9 @@
 include "basics/lists/list.ma".
 include "basics/lists/listb.ma".
+include "Clight/SimplifyCasts.ma".
+
 
 
@@ -204 +206 @@
      normalize @conj try @conj try @conj try @conj try //
      @(convert_break_lift ?? Hsf)
-] qed.
+] qed. 
 
 (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
    order to circumvent the associativity problems in notations. *)
+(*
 record swret (A : Type[0]) : Type[0] ≝ {
   ret_st  : A;
   ret_acc : list (ident × type);
-  ret_fvs : list ident;
   ret_u   : universe SymbolTag
 }.
 
-notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
-for @{ match ${e} with
-       [ None ⇒ None ?
-       | Some ${fresh ret} ⇒
-          (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
-          (ret_st ? ${fresh ret})
-          (ret_acc ? ${fresh ret})
-          (ret_fvs ? ${fresh ret})
-          (ret_u ? ${fresh ret}) ] }.
-
-notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
-for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
+notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48
+for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'})
+          (ret_st ? ${e})
+          (ret_acc ? ${e})
+          (ret_u ? ${e}) }.
+
+definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *)
       
 (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
@@ -234 +231 @@
 let rec switch_removal
   (st : statement)           (* the statement in which we will remove switches *)
-  (fvs : list ident)         (* a finite list of names usable to create variables. *)
-  (u : universe SymbolTag)   (* a fresh /label/ generator *)
-  : option (swret statement) ≝
+  (u : universe SymbolTag)   (* a fresh label and ident generator *)
+  : statement × (list (ident × type)) × (universe SymbolTag) ≝
 match st with
-[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
-| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
-| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
+[ Sskip       ⇒ 〈st, [ ], u〉
+| Sassign _ _ ⇒ 〈st, [ ], u〉
+| Scall _ _ _ ⇒ 〈st, [ ], u〉
 | Ssequence s1 s2 ⇒
-  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
-  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
-  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
+  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
+  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
+  〈Ssequence s1' s2', acc1 @ acc2, u''〉
 | Sifthenelse e s1 s2 ⇒
-  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
-  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
-  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
+  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
+  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
+  〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉
 | Swhile e body ⇒
-  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Swhile e body', acc, fvs', u'〉
+  let 〈body', acc, u'〉 ≝ switch_removal body u in
+  〈Swhile e body', acc, u'〉
 | Sdowhile e body ⇒
-  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Sdowhile e body', acc, fvs', u'〉
+  let 〈body', acc, u'〉 ≝ switch_removal body u in
+  〈Sdowhile e body', acc, u'〉
 | Sfor s1 e s2 s3 ⇒
-  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
-  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
-  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
-  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
+  let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in
+  let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in
+  let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in
+  〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉
 | Sbreak ⇒
-  ret 〈st, [ ], fvs, u〉
+  〈st, [ ], u〉
 | Scontinue ⇒
-  ret 〈st, [ ], fvs, u〉
+  〈st, [ ], u〉
 | Sreturn _ ⇒
-  ret 〈st, [ ], fvs, u〉
+  〈st, [ ], u〉
 | Sswitch e branches ⇒   
-   do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
-   match fvs' with
-   [ nil ⇒ None ?
-   | cons fresh tl ⇒
-     (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
-     let ident         ≝ Expr (Evar fresh) (typeof e) in
-     let assign        ≝ Sassign ident e in
-     let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
-       ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
-   ]
+  let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in
+  let 〈switch_tmp, u''〉 ≝ fresh ? u' in
+  let ident         ≝ Expr (Evar switch_tmp) (typeof e) in
+  let assign        ≝ Sassign ident e in
+  let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in
+  〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉
 | Slabel label body ⇒
-  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Slabel label body', acc, fvs', u'〉
+  let 〈body', acc, u'〉 ≝ switch_removal body u in
+  〈Slabel label body', acc, u'〉
 | Sgoto _ ⇒
-  ret 〈st, [ ], fvs, u〉
+  〈st, [ ], u〉
 | Scost cost body ⇒
-  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Scost cost body', acc, fvs', u'〉 
+  let 〈body', acc, u'〉 ≝ switch_removal body u in
+  〈Scost cost body', acc, u'〉
 ]
 
 and switch_removal_branches 
   (l : labeled_statements) 
-  (fvs : list ident) 
   (u : universe SymbolTag)
-(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
+ : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝
 match l with
 [ LSdefault st ⇒
-  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
-  ret 〈LSdefault st', acc1, fvs', u'〉
-| LScase sz int st tl =>
-  do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
-  do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
-  ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
+  let 〈st', acc1, u'〉 ≝ switch_removal st u in
+  〈LSdefault st', acc1, u'〉
+| LScase sz int st tl ⇒
+  let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in
+  let 〈st', acc2, u''〉 ≝ switch_removal st u' in
+  〈LScase sz int st' tl_result, acc1 @ acc2, u''〉
 ].
 
-let rec mk_fresh_variables
-  (st : statement)           (* the statement in which we will remove switches *)
-  (u : universe SymbolTag)   (* a fresh /label/ generator *)
-  : (list ident) × (universe SymbolTag) ≝
-match st with
-[ Sskip       ⇒ 〈[ ], u〉
-| Sassign _ _ ⇒ 〈[ ], u〉
-| Scall _ _ _ ⇒ 〈[ ], u〉
-| Ssequence s1 s2 ⇒
-  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
-  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
-  〈fvs @ fvs', u''〉
-| Sifthenelse e s1 s2 ⇒
-  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
-  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
-  〈fvs @ fvs', u''〉
-| Swhile e body ⇒
-  mk_fresh_variables body u
-| Sdowhile e body ⇒
-  mk_fresh_variables body u
-| Sfor s1 e s2 s3 ⇒
-  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
-  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
-  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
-  〈fvs @ fvs' @fvs'', u'''〉
-| Sbreak ⇒
-  〈[ ], u〉
-| Scontinue ⇒
-  〈[ ], u〉
-| Sreturn _ ⇒
-  〈[ ], u〉
-| Sswitch e branches ⇒   
-   let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
-   let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
-   〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
-| Slabel label body ⇒
-  mk_fresh_variables body u
-| Sgoto _ ⇒
-  〈[ ], u〉
-| Scost cost body ⇒
-  mk_fresh_variables body u
-]
-
-and mk_fresh_variables_branches 
-  (l : labeled_statements) 
-  (u : universe SymbolTag)
-(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
-match l with
-[ LSdefault st ⇒
-  mk_fresh_variables st u
-| LScase sz int st tl =>
-  let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
-  let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
-  〈fvs @ fvs', u''〉
-].
-
-(* Copied this from Csyntax.ma, lifted from Prop to Type 
-   (I needed to eliminate something proved with this towards Type)  *)
-let rec statement_indT
-  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
-  (Ssk:P Sskip)
-  (Sas:∀e1,e2. P (Sassign e1 e2))
-  (Sca:∀eo,e,args. P (Scall eo e args))
-  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
-  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s. P s → P (Swhile e s))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
-  (Sbr:P Sbreak)
-  (Sco:P Scontinue)
-  (Sre:∀eo. P (Sreturn eo))
-  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
-  (Sla:∀l,s. P s → P (Slabel l s))
-  (Sgo:∀l. P (Sgoto l))
-  (Scs:∀l,s. P s → P (Scost l s))
-  (LSd:∀s. P s → Q (LSdefault s))
-  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
-  (s:statement) on s : P s ≝
-match s with
-[ Sskip ⇒ Ssk
-| Sassign e1 e2 ⇒ Sas e1 e2
-| Scall eo e args ⇒ Sca eo e args
-| Ssequence s1 s2 ⇒ Ssq s1 s2
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-| Swhile e s ⇒ Swh e s
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sdowhile e s ⇒ Sdo e s
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
-| Sbreak ⇒ Sbr
-| Scontinue ⇒ Sco
-| Sreturn eo ⇒ Sre eo
-| Sswitch e ls ⇒ Ssw e ls
-    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
-| Slabel l s ⇒ Sla l s
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sgoto l ⇒ Sgo l
-| Scost l s ⇒ Scs l s
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-]
-and labeled_statements_indT
-  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
-  (Ssk:P Sskip)
-  (Sas:∀e1,e2. P (Sassign e1 e2))
-  (Sca:∀eo,e,args. P (Scall eo e args))
-  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
-  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s. P s → P (Swhile e s))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
-  (Sbr:P Sbreak)
-  (Sco:P Scontinue)
-  (Sre:∀eo. P (Sreturn eo))
-  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
-  (Sla:∀l,s. P s → P (Slabel l s))
-  (Sgo:∀l. P (Sgoto l))
-  (Scs:∀l,s. P s → P (Scost l s))
-  (LSd:∀s. P s → Q (LSdefault s))
-  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
-  (ls:labeled_statements) on ls : Q ls ≝
-match ls with
-[ LSdefault s ⇒ LSd s
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| LScase sz i s t ⇒ LSc sz i s t
-    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
-].
-
-lemma switch_removal_ok :
-  ∀st, u0, u1, post.
-  Σresult. 
-  (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
-#st 
-@(statement_indT ? (λls. ∀u0, u1, post. 
-                          Σresult.
-                          (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
-                          ∧ (ret_fvs ? result = post)
-                   ) … st)
-[ 1: #u0 #u1 #post normalize
-     %{(mk_swret statement Sskip [] post u1)} % //
-| 2: #e1 #e2 #u0 #u1 #post normalize
-     %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
-| 3: #e0 #e #args #u0 #u1 #post normalize
-     %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
-| 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
-     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *      
-     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
-     elim (H2 u' (ret_u ? s1') post) #s2' *
-     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
-     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
-     %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
-        (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
-        (ret_u statement s2'))} % try //
-| 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
-     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *      
-     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
-     elim (H2 u' (ret_u ? s1') post) #s2' *
-     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
-     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
-     %{((mk_swret statement
-         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
-         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
-         (ret_u statement s2')))} % try //
-| 6: #e #s #H #u0 #u1 #post normalize
-     elim (H u0 u1 post) #s1' * normalize
-     cases (mk_fresh_variables s u0) #fvs #u'
-     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
-     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
-        (ret_fvs statement s1') (ret_u statement s1'))} % try //
-| 7: #e #s #H #u0 #u1 #post normalize
-     elim (H u0 u1 post) #s1' * normalize
-     cases (mk_fresh_variables s u0) #fvs #u'
-     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
-     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
-        (ret_fvs statement s1') (ret_u statement s1'))} % try //
-| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
-     elim (H1 u0 u1
-                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
-                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
-                post)) #s1' *
-     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
-     elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
-                                 post)) #s2' *
-     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
-     elim (H3 u'' (ret_u ? s2') post) #s3' *
-     cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
-     #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
-     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
-     >Heq2 normalize >Heq2_fvs >Heq3 normalize
-     %{(mk_swret statement
-        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
-        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
-        (ret_fvs statement s3') (ret_u statement s3'))} % try //
-| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
-| 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
-| 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
-| 12: #e #ls #H #u0 #u1 #post
-      whd in match (mk_fresh_variables ??);
-      whd in match (switch_removal ???);      
-      elim (fresh ? u0) #fresh #u'
-      elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
-      cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta      
-      >associative_append #Heq #Heq_fvs >Heq normalize nodelta
-      >Heq_fvs normalize nodelta
-      cases (simplify_switch ???) #st' #u''' normalize nodelta
-      %{((mk_swret statement
-          (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
-          (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
-          (ret_u labeled_statements ls')))} % //
-| 13: #l #s #H #u0 #u1 #post normalize
-      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
-      %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
-           post (ret_u statement s'))} % //
-| 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
-| 15: #l #s #H #u0 #u1 #post normalize
-      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
-      %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
-           post (ret_u statement s'))} % //
-| 16: #s #H #u0 #u1 #post normalize
-      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
-      %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
-         (ret_acc statement s') post (ret_u statement s'))} % //
-| 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
-      elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
-      cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
-      elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
-      cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
-      >associative_append >Heql normalize >Heql_fvs >Heq normalize
-      %{(mk_swret labeled_statements
-          (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
-          (ret_acc labeled_statements ls'@ret_acc statement s1')
-          (ret_fvs statement s1') (ret_u statement s1'))} % //
-] qed.
+definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝ 
+λA,x.
+  let 〈s,vars,u〉 ≝ x in s.
+
+definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝ 
+λA,x.
+  let 〈s,vars,u〉 ≝ x in vars.
+
+definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝ 
+λA,x.
+  let 〈s,vars,u〉 ≝ x in u.
 
 axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
 
 (* Proof that switch_removal_switch_free does its job. *)
-lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
-#st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result → 
-                                                 branches_switch_free (ret_st ? ls_result)) … st)
-[ 1: #fvs #u #result normalize #Heq destruct (Heq) //
-| 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
-| 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
-| 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
-     elim (switch_removal s1 fvs u) normalize
-     [ 1: #_ #Habsurd destruct (Habsurd)
-     | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
-          elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
-          [ 1: normalize #_ #Habsurd destruct (Habsurd)
-          | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
-               normalize @conj
-               [ 1: @Heq1 // | 2: @Heq2 // ]
-     ] ]
+lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)).
+#st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st)
+try //
+[ 1: #s1 #s2 #H1 #H2 #u normalize
+     lapply (H1 u)
+     cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA
+     lapply (H2 u') 
+     cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB
+     @conj assumption
 | *: 
   (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
@@ -623 +378 @@
   max_id (max_of_expr f) 
          (max_id retmax
-                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
+                 (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) )
 | Ssequence s1 s2 ⇒
   max_id (max_of_statement s1) (max_of_statement s2)
@@ -663 +418 @@
 definition function_switch_removal : function → function × (list (ident × type)) ≝ 
 λf.
-  (λres_record.
-    let new_vars ≝ ret_acc ? res_record in
-    let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
-    〈result, new_vars〉)
-  (let u ≝ universe_of_max (max_id_of_function f) in
-   let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
-   match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
-   [ None ⇒ λHsr. ?
-   | Some res_record ⇒ λ_. res_record
-   ] (refl ? (switch_removal (fn_body f) fvs u'))).    
-lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
-<Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
-qed.
+  let u ≝ universe_of_max (max_id_of_function f) in
+  let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in
+  let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in
+  〈result, vars〉.
 
 let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
@@ -695 +441 @@
   sf_funcs
   (prog_main … p).
-
 
 (* -----------------------------------------------------------------------------
@@ -742 +487 @@
 #H1 #H2 destruct (H2) /2/ qed.
 
-lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
-#u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh) 
-cases (fresh SymbolTag u)
-#fv #u' #H %{fv} %{u'} @conj try // @H //
-qed.
+definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ 
+λu1,u2.
+  match u1 with
+  [ mk_universe p1 ⇒
+    match u2 with
+    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
+    
+definition fte ≝ fresher_than_or_equal.
+
+lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
+* #u1 * #u2 * #u3 normalize /2 by transitive_le/
+qed.
+
+lemma reflexive_fte : ∀u. fte u u.
+* // qed.
+
+lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1.
+* #p * #p' normalize #H * #i normalize 
+/2 by transitive_le/
+qed.
+
+lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2.
+* #u1 * #u2 * #fv normalize #H1 destruct //
+qed.
+
+lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u.
+#e #exit #ls @(branches_ind … ls)
+[ 1: #st #u normalize lapply (fresh_fte u)
+     cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize //
+| 2: #sz #i #hd #tl #Hind #u normalize
+     lapply (Hind u) cases (produce_cond e tl u exit) *
+     #subcond #sublabel #u1 #Hfte normalize
+     lapply (fresh_fte u1)
+     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??))
+     #Hfte' normalize cases u2 in Hfte'; #u2
+     cases u in Hfte; #u cases u1 #u1 normalize
+     /2 by transitive_le/
+] qed.
 
 lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
-#e #exit #ls @(branches_ind … ls)
-[ 1: #st #u #i #Hfresh normalize
-     lapply (fresh_for_univ_still_fresh … Hfresh)
-     cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
-| 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
-     lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
-     #subcond #sublabel #u1 #Hfresh1 normalize
-     lapply (fresh_for_univ_still_fresh … Hfresh1)
-     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
-] qed.
-
-lemma simplify_switch_fresh : ∀u,i,e,ls. 
- fresh_for_univ ? i u → 
+#e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed.
+
+lemma simplify_switch_fte : ∀u,e,ls. 
+  fte (\snd (simplify_switch e ls u)) u.
+#u #e #ls normalize
+lapply (fresh_fte u)
+cases (fresh ? u)
+#exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux
+normalize
+lapply (produce_cond_fte e exit_label ls uv1)
+cases (produce_cond ????) * #stm #label #uv2 normalize nodelta
+cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize
+/2 by transitive_le/
+qed.
+
+lemma simplify_switch_fresh : ∀u,i,e,ls.
+ fresh_for_univ ? i u →
  fresh_for_univ ? i (\snd (simplify_switch e ls u)).
-#u #i #e #ls #Hfresh
-normalize
-lapply (fresh_for_univ_still_fresh … Hfresh)
-cases (fresh ? u)
-#exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
-normalize lapply (produce_cond_fresh e exit_label ls … Haux)
-elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
-qed.
+#u #i #e #ls @fresher_for_univ @simplify_switch_fte qed.
+
+lemma switch_removal_fte : ∀st,u.
+  fte (ret_u ? (switch_removal … st u)) u.
+#st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st)
+try /2 by reflexive_fte/
+[ 1: #s1 #s2 #Hind1 #Hind2 #u normalize
+     lapply (Hind1 u)
+     cases (switch_removal s1 u) * #s1' #fvs1 #u'  normalize nodelta
+     lapply (Hind2 u')
+     cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize
+     #HA #HB @(transitive_fte … HA HB)
+| 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize
+     lapply (Hind1 u)
+     cases (switch_removal s1 u) * #s1' #fvs1 #u'  normalize nodelta
+     lapply (Hind2 u')
+     cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize
+     #HA #HB @(transitive_fte … HA HB)
+| 3,7,8: #e #s #Hind #u normalize
+     lapply (Hind u)
+     cases (switch_removal s u) * #s' #fvs #u' normalize #H @H
+| 4: #e #s #Hind #u normalize
+     lapply (Hind u)
+     cases (switch_removal s u) * #s' #fvs #u' normalize #H @H
+| 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize
+     lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1
+     normalize nodelta
+     lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2
+     normalize nodelta
+     lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3
+     normalize nodelta
+     /3 by transitive_fte/
+| 6: #e #ls #Hind #u whd in match (switch_removal ??);
+     lapply (Hind u)
+     cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1
+     normalize nodelta
+     lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2
+     normalize nodelta
+     lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls)
+     cases (simplify_switch ???) 
+     normalize nodelta
+     #st' #u''' #Hfte3
+     /3 by transitive_fte/
+| 9: #s #H #u normalize
+     lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H
+| 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize
+     lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u'
+     normalize nodelta #Hfte1
+     lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u''
+     normalize nodelta #Hfte2
+     /3 by transitive_fte/
+] qed.     
+
+lemma switch_removal_fresh : ∀u,i,st.
+  fresh_for_univ ? i u →
+  fresh_for_univ ? i (ret_u … (switch_removal st u)).
+#u #i #st @fresher_for_univ @switch_removal_fte qed.
 
 (* -----------------------------------------------------------------------------
@@ -879 +710 @@
 ] qed.
 
+lemma fresh_to_substatements :
+  ∀s,u. fresh_for_statement s u → 
+        substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
+#s #u cases s
+whd in match (fresh_for_statement ??);
+whd in match (substatement_P ???); try /2/
+[ 1: #e1 #e2
+     whd in match (fresh_for_statement ??);
+     whd in match (substatement_P ???);
+     #H lapply (fresh_max_split … H) * /2 by conj/     
+| 2: #e1 #e2 #args
+     whd in match (fresh_for_statement ??);
+     whd in match (substatement_P ???);
+     cases e1 normalize nodelta
+     [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA
+          elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB
+          elim (fresh_max_split … HB) #HC #HD
+          whd in match (foldr ?????) in HD;
+          elim (fresh_max_split … HD) #HE #HF
+          @conj try assumption
+          @Hind >max_id_commutative >max_id_one_neutral @HF
+     | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB
+          cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try //
+          #e #l #Hind #HD
+          whd in match (foldr ?????) in HD;
+          elim (fresh_max_split … HD) #HE #HF
+          @conj try assumption
+          @Hind @HF ]
+| 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split
+| 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) *
+     #H1 @fresh_max_split
+| 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H)
+| 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H)
+| 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2
+     @conj try @conj try @I try @conj try @I
+     elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/
+| 8: #opt cases opt try /2/
+| 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB
+     @(labeled_statements_ind … ls)
+     [ 1: #s' #H' //
+     | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj
+          [ 1: //
+          | 2: @Hind @H1 ] ]
+| 10: #lab #stmt #H whd lapply (fresh_max_split … H) * //
+] qed.
+
 (* Auxilliary commutation lemma used in [substatement_fresh]. *)
-
 lemma foldl_max : ∀l,a,b. 
   foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = 
@@ -945 +821 @@
 definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.
 
-definition outbound_pointer ≝ λm,p. 
-   Zltb (block_id (pblock p)) (nextblock m) = true ∧
-   Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧
-   high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)).
-   
-(* a valid_pointer is either /inside/ the bounds of the target block xor /one off/ the end.  *)
-lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p.
+lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p.
 #m #p @conj
 [ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
-     whd in match (outbound_pointer ??);
      whd in match (do_if_in_bounds); normalize nodelta
      cases (Zltb (block_id (pblock p)) (nextblock m))
-     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]     
+     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
      >andb_lsimpl_true normalize nodelta
      cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
      [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
      >andb_lsimpl_true normalize nodelta
-     lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
-     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
-     [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/
-     | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ]
-| 2: whd in match (valid_pointer ??); *
-     [ 1: whd in match (in_bounds_pointer ??); #H
-          lapply (H bool (λblock,contents,off. true))
-          * #foo whd in match (do_if_in_bounds ????);
-          cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
-          [ 2: #Habsurd destruct (Habsurd) ]
-          >andb_lsimpl_true 
-          cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
-          normalize nodelta
-          [ 2: #Habsurd destruct (Habsurd) ]
-          >andb_lsimpl_true
-          elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
-          [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl
-          | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
-     | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb 
-          #Hhigh >Hhigh >andb_lsimpl_true 
-          lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p))))
-          #Hle >(Zle_to_Zleb_true … Hle) @refl
-     ]
-] qed.
+     #Hlt >Hlt normalize nodelta #A #f /2 by ex_intro/
+| 2: whd in match (valid_pointer ??);
+     whd in match (in_bounds_pointer ??); #H
+     lapply (H bool (λblock,contents,off. true))
+     * #foo whd in match (do_if_in_bounds ????);
+     cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
+     [ 2: #Habsurd destruct (Habsurd) ]
+     >andb_lsimpl_true 
+     cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
+     normalize nodelta
+     [ 2: #Habsurd destruct (Habsurd) ]
+     >andb_lsimpl_true
+     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))     
+     [ 1: #H >H //
+     | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
+] qed.
+
+lemma valid_pointer_to_Prop : 
+  ∀m,p. valid_pointer m p = true →
+        (block_id (pblock p)) < (nextblock m) ∧
+        (low_bound m (pblock p)) ≤ (Z_of_unsigned_bitvector offset_size (offv (poff p))) ∧
+        (Z_of_unsigned_bitvector offset_size (offv (poff p))) < (high_bound m (pblock p)).
+#m #p whd in match (valid_pointer ??);        
+#H 
+lapply (Zleb_true_to_Zle (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
+lapply (Zltb_true_to_Zlt (block_id (pblock p)) (nextblock m)) 
+cases (Zltb (block_id (pblock p)) (nextblock m)) in H;
+[ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
+cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
+normalize nodelta
+[ 2: #Habsurd destruct ]
+#Hlt1 #Hlt2 #Hle @conj try @conj
+try @(Hlt2 (refl ??)) try @(Hle (refl ??)) @(Zltb_true_to_Zlt … Hlt1)
+qed.
 
 (* A writeable_block is a block that is:
@@ -995 +874 @@
   wb_valid      : valid_block m b;
   wb_nonempty   : low (blocks m b) < high (blocks m b)
-}. 
+}.
 
 (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *)
@@ -1004 +883 @@
   me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b;
   (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *)
-  me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable);
-  (* This field does not entail [me_not_writeable] and is necessary to prove valid
+  me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable)
+  
+  (* This field is not entailed [me_not_writeable] and is necessary to prove valid
      pointer conservation after a [free]. *)
-  me_not_writeable_ptr : ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable);
-  
+
   (* Extension blocks contain nothing in [m1] *)
   (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ;  *)
@@ -1019 +898 @@
      compare are valid before being equal).
   *)
-  me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *)
+(*  me_valid_pointers : ∀p.
                        valid_pointer m1 p = true → 
-                       valid_pointer m2 p = true
+                       valid_pointer m2 p = true *)
 }.
+
+(* Since we removed end_pointers, we can prove some stuff that was previously given as a field of
+   sr_memext. *)
+lemma me_not_writeable_ptr : 
+  ∀m1,m2,writeable. 
+  sr_memext m1 m2 writeable → 
+  ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable).
+#m1 #m2 #writeable #Hext #p #Hvalid
+cut (nonempty_block m1 (pblock p))
+[ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % //
+     /2 by Zle_to_Zlt_to_Zlt/
+| 2: @(me_not_writeable … Hext) ]
+qed.
 
 (* If we have a memory extension, we can simulate loads *)
@@ -1052 +944 @@
 >(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize
 >Hres @refl
+qed.
+
+lemma me_valid_pointers : 
+  ∀m1,m2,writeable. 
+  sr_memext m1 m2 writeable → 
+  ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true.
+* #contents1 #nextblock1 #Hnextblock_pos1
+* #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid
+cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb)
+[ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % //
+     /2 by Zle_to_Zlt_to_Zlt/ ]
+#Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high
+#Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta
+<Hcontents_eq cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt
+>(Zle_to_Zleb_true … Hle) normalize nodelta
+>(Zlt_to_Zltb_true … Hlt) @refl
 qed.
 
@@ -1087 +995 @@
           lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ]
 ] qed.          
-            
+
 lemma environment_sim_invert : 
   ∀en1,en2. environment_sim en1 en2 →
@@ -1206 +1114 @@
      ]
 ] qed.
-
 
 lemma blocks_of_env_cons : 
@@ -1346 +1253 @@
 [ 1: #b #H @conj try % elim H try //
 | 2: #b *
-| 3: #b #_ normalize % //
-| 4: #p #Hvalid % *
-(* | 4: #b * *)
-| 5: #p normalize >Hcontents_eq #H @H
-] qed.
+| 3: #b #_ normalize % // ]
+qed.
 
 (* memory extensions form a preorder relation *)
@@ -1374 +1278 @@
           lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption
      ]
-| 4: #p #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) *
-     [ 1: #Hmem12
-          lapply (me_not_writeable_ptr … H12 … Hvalid) * #H @H assumption
-     | 2: #Hmem23
-          lapply (me_valid_pointers … H12 … Hvalid) #Hvalid2
-          lapply (me_not_writeable_ptr … H23 … Hvalid2) * #H @H assumption
-     ]          
-| 5: #p #Hvalid @(me_valid_pointers … H23) @(me_valid_pointers … H12) @Hvalid
-] qed.
-
-lemma memory_ext_reflexive : 
-  ∀m. sr_memext m m [ ].
+] qed.     
+
+lemma memory_ext_reflexive : ∀m. sr_memext m m [ ].
 #m % /2/ #b * qed.
 
@@ -1456 +1351 @@
 >andb_lsimpl_true
 normalize nodelta #H
-@Zltb_to_Zleb_true
 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
 try // normalize #Habsurd destruct (Habsurd)
+qed.
+
+lemma bestorev_to_valid_pointer : ∀m,ptr,v,res. bestorev m ptr v = Some ? res → valid_pointer m ptr = true.
+* #contents #next #nextpos #ptr #v #res
+whd in match (bestorev ???);
+whd in match (valid_pointer ??);
+cases (Zltb (block_id (pblock ptr)) next)
+normalize nodelta
+[ 2: #Habsurd destruct (Habsurd) ]
+>andb_lsimpl_true
+whd in match (low_bound ??);
+whd in match (high_bound ??);
+cases (Zleb (low (contents (pblock ptr)))
+        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
+[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
+>andb_lsimpl_true
+cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr))))
+normalize nodelta try // #Habsurd destruct (Habsurd)
 qed.
 
@@ -1557 +1469 @@
 qed.
 
+(* If a pointer is still valid after a free (meaning we freed another block), then it was valid before. *)
 lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
 #m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
 #H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
 elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
-[ 1: #Hlt >Hlt normalize nodelta 
+[ 1: #Hlt >Hlt normalize nodelta
      @(eq_block_elim … b (pblock p))
      [ 1: #Heq >Heq whd in match (free ??);
@@ -1583 +1496 @@
 qed.
 
-lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p.
-#m #b #p whd in match (free ??);
-whd in match (outbound_pointer ??) in ⊢ (% → %);
-whd in match (update_block ????);
-whd in match (low_bound ??); whd in match (high_bound ??);
-@(eq_block_elim … (pblock p) b) normalize nodelta
-[ 1: #Heq >Heq cases (Zltb ? (nextblock m))
-     [ 2: * * #Habsurd destruct (Habsurd) ]
-     * * #_ whd in match (low ?); whd in match (high ?);
-     #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
-| 2: #Hneq #H @H ]
-qed.
-
+(* Cf [in_bounds_free_to_in_bounds] *)
 lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
 #m #b #p #Hvalid
-lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef
-elim (valid_pointer_def … (free m b) p) #H #_
-elim (H Hvalid)
-[ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption
-| 2: #Hout %2 @outbound_free_to_outbound assumption ]
-qed.
-
+cases (valid_pointer_def … m p) #HA #HB
+cases (valid_pointer_def … (free m b) p) #HC #HD
+@HB @(in_bounds_free_to_in_bounds … b)
+@HC @Hvalid
+qed.
+
+(* Making explicit the argument above. *)
 lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
 #m #b #p
@@ -1613 +1514 @@
 whd in match (high_bound ??);
 @(eq_block_elim … b (pblock p))
-[ 1: #Heq >Heq >eq_block_b_b normalize nodelta
+[ 1: #Heq <Heq >eq_block_b_b normalize nodelta
      whd in match (low ?); whd in match (high ?);
      cases (Zltb ? (nextblock m))
@@ -1621 +1522 @@
 qed.
 
+(* Lifting the property of being valid after a free to memory extensions *)
 lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true.
 #m1 #m2 #writeable #Hext #p #b #Hvalid
@@ -1703 +1605 @@
           ]
      ]
-| 4: #p #Hvalid 
-     lapply (valid_free_to_valid … Hvalid) #Hvalid'
-     lapply (me_not_writeable_ptr … Hext … Hvalid') * #HA % #HB @HA     
-     elim writeable in HB;
-     [ 1: *
-     | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block
-          @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
-          [ 1: #Heq #H normalize %2 @(Hind H)
-          | 2: #Hblocks_neq whd in match (meml ???); *
-               [ 1: #Hneq normalize %1 assumption
-               | 2: #Hmem normalize %2 @(Hind Hmem) ]
-          ]
-     ]
-| 5: #p @(valid_pointer_free … writeable) @Hext
-] qed.
+] qed.     
+
 
 (* Freeing from an extension block is ok. *) 
@@ -1769 +1658 @@
      ] ] ] * #Hmem' #Hblocks_neq
      lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
-| 4: #p #Hnonempty % #Hmem
-     cut (mem block (pblock p) writeable ∧ (pblock p) ≠ b)
-     [ elim writeable in Hmem;
-       [ 1: normalize @False_ind
-       | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block
-            @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta
-            [ 1: #Heq #H whd in match (meml ???); destruct
-                 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption
-            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
-                 [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] 
-                 | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ]
-     ] ] ] * #Hmem' #Hblocks_neq
-     lapply (me_not_writeable_ptr … Hext … Hnonempty) * #H @H assumption 
-| 5: #p #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_mem
-     lapply (mem_not_mem_neq … Hb_writeable … Hnot_mem) #Hneq
-     lapply (me_valid_pointers … Hext … Hvalid) #Hvalid'
-     whd in match (free ??);
-     whd in match (valid_pointer ??) in ⊢ (??%%);
-     whd in match (low_bound ??); whd in match (high_bound ??);
-     whd in match (update_block ?????);
-     >(not_eq_block_rev … Hneq) normalize
-     @Hvalid'
-] qed.
-
-
+] qed.
   
   
@@ -1881 +1746 @@
     sr_memext m1 m2 (hd :: writeable) →
     sr_memext m1 m2 writeable.
-#m1 #m2 #hd #writeable * 
-#Hnonempty #Hwriteable_valid #Hnot_writeable #Hnot_writeable_ptr #Hvalid_pointers %
+#m1 #m2 #hd #writeable *
+#Hnonempty #Hwriteable_valid #Hnot_writeable %
 try assumption
 [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption
 | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem
-| 3: #p #Hvalid % #Hmem elim (Hnot_writeable_ptr … Hvalid) #H @H whd %2 @Hmem
 ] qed.
 
@@ -1902 +1766 @@
      lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
      lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
-| 4: #p #Hvalid % #Hmem
-     lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
-     lapply (me_not_writeable_ptr … Hext … Hvalid) * #H @H assumption
-| 5: @(me_valid_pointers … Hext) ]
-qed.
-
-axiom lset_inclusion_difference :
+] qed.     
+
+lemma lset_difference_empty :
   ∀A : DeqSet.
-  ∀s1,s2 : lset (carr A).
-    lset_inclusion ? s1 s2 →
-    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
-          lset_disjoint ? s1 s2' ∧
-          lset_eq ? s2' (lset_difference ? s2 s1).
-          
-lemma memory_eq_to_memory_ext_pre :
-  ∀m1,m1',m2,writeable.
-  memory_eq m1 m1' →
-  sr_memext m1' m2 writeable →
-  sr_memext m1 m2 writeable.
-#m1 #m1' #m2 #writeable #Heq #Hext
-lapply (memory_eq_to_mem_ext … Heq) #Hext'
-@(memory_ext_transitive … Hext' Hext)
-qed.
-
-lemma memory_eq_to_memory_ext_post :
-  ∀m1,m2,m2',writeable.
-  memory_eq m2' m2 →
-  sr_memext m1 m2' writeable →
-  sr_memext m1 m2 writeable.
-#m1 #m2 #m2' #writeable #Heq #Hext
-lapply (memory_eq_to_mem_ext … Heq) #Hext'
-lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
+  ∀s1. lset_difference A s1 [ ] = s1.
+#A #s1 elim s1 try //
+#hd #tl #Hind >lset_difference_unfold >Hind @refl
 qed.
 
@@ -1946 +1785 @@
      | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
 ] qed.
-
-lemma lset_difference_nil : ∀A,s. lset_difference A s [ ] = s. #A #s elim s //
-#hd #tl #Hind >lset_difference_unfold normalize in match (memb ???); normalize nodelta >Hind @refl
-qed.
 
 lemma lset_mem_inclusion_mem :
@@ -2049 +1884 @@
                 [ 1: %2 @Hind @Hmem
                 | 2: @Hind @Hmem ] ] ]
-] qed.                
+] qed.
+
+lemma lset_disjoint_dec : 
+  ∀A : DeqSet.
+  ∀s1,elt,s2.
+  mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1).
+#A #s1 #elt #s2
+@(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ?
+  with
+  [ false ⇒ λHA. ?
+  | true ⇒ λHA. ? ] (refl ? (elt ∈ s1)))
+[ 1: lapply (memb_to_mem … HA) #Hmem
+     %1 @Hmem
+| 2: %2 elim s1 in HA;
+     [ 1: #_ whd %1 @refl
+     | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?);
+          >lset_difference_unfold
+          >lset_difference_unfold2
+          lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %);
+          cases (elt==hd1) normalize nodelta
+          [ 1: #_ #Habsurd destruct
+          | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ]
+qed.
+
+lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2.
+  mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l.
+#A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/
+qed.
+
+lemma lset_inclusion_difference_aux :
+  ∀A : DeqSet. ∀s1,s2.
+  lset_inclusion A s1 s2 →
+  (lset_eq A s2 (s1@lset_difference A s2 s1)).
+#A #s1
+@(WF_ind ????? (filtered_list_wf A s1))
+*
+[ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq
+| 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl
+     lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?)
+     [ 1: whd normalize
+          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ]
+     #Hind_wf      
+     elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq 
+     >cons_to_append in ⊢ (???%); >associative_append
+     >lset_difference_unfold2
+     >nil_append
+     >lset_remove_split >lset_remove_split
+     normalize in match (lset_remove ? [hd1] hd1);
+     >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
+     >nil_append <lset_remove_split >lset_difference_lset_remove_commute
+     lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?)
+     [ 1: lapply (lset_inclusion_remove … Hincl hd1)
+          >Heq @lset_inclusion_eq2
+          >lset_remove_split >lset_remove_split >lset_remove_split
+          normalize in match (lset_remove ? [hd1] hd1);
+          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
+          >nil_append @reflexive_lset_eq ]
+     #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind
+     @lset_eq_concrete_to_lset_eq
+     lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc
+     @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind
+     [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B))
+          [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete
+          | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ]
+     | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …))
+          elim (s2A@s2B)
+          [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq
+          | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold
+               @(match (hd2∈filter A (λx:A.¬x==hd1) tl1)
+                 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ?
+                 with
+                 [ false ⇒ λH. ?
+                 | true ⇒ λH. ?
+                 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta
+               [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter))
+                    normalize nodelta @Hind
+               | 2: @(match (hd2∈tl1)
+                      return λx. ((hd2∈tl1) = x) → ?
+                      with
+                      [ false ⇒ λH'. ?
+                      | true ⇒ λH'. ?
+                      ] (refl ? (hd2∈tl1))) normalize nodelta
+                      [ 1: (* We have hd2 = hd1 *)
+                            cut (hd2 = hd1)
+                            [ elim tl1 in H H';
+                              [ 1: normalize #_ #Habsurd destruct (Habsurd)
+                              | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?);
+                                    lapply (eqb_true ? hdtl1 hd1)
+                                    cases (hdtl1==hd1) normalize nodelta
+                                    [ 1: * #H >(H (refl ??)) #_
+                                         lapply (eqb_true ? hd2 hd1)
+                                         cases (hd2==hd1) normalize nodelta *
+                                         [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl
+                                         | 2: #_ #_ @Hind ]
+                                    | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1)
+                                         cases (hd2 == hdtl1) normalize nodelta *
+                                         [ 1: #_ #_ #Habsurd destruct (Habsurd)
+                                         | 2: #_ #_ @Hind ] ] ] ]
+                           #Heq_hd2hd1 destruct (Heq_hd2hd1)
+                           @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind)
+                           #Hind' @(square_lset_eq_concrete … Hind')
+                           [ 2: @lset_refl
+                           | 1: >cons_to_append >cons_to_append in ⊢ (???%);
+                                @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
+                                [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract
+                                | 2: >(cons_to_append … hd1 (lset_difference ???)) 
+                                     @lset_eq_concrete_cons >nil_append >nil_append
+                                     @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ]
+                        | 2: @(match hd2 == hd1
+                               return λx. ((hd2 == hd1) = x) → ?
+                               with
+                               [ true ⇒ λH''. ?
+                               | false ⇒ λH''. ?
+                               ] (refl ? (hd2 == hd1)))
+                             [ 1: whd in match (lset_remove ???) in ⊢ (???%);
+                                  >H'' normalize nodelta >((proj1 … (eqb_true …)) H'')
+                                  @(transitive_lset_eq … Hind)
+                                  @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
+                                  [ 2: @lset_eq_contract ]                                                                   
+                                  @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons                                  
+                                  @switch_lset_eq_concrete
+                             | 2: whd in match (lset_remove ???) in ⊢ (???%);
+                                  >H'' >notb_false normalize nodelta
+                                  @lset_eq_concrete_to_lset_eq
+                                  lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc
+                                  lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc
+                                  @(square_lset_eq_concrete … Hindc')
+                                  [ 1: @symmetric_lset_eq_concrete 
+                                       >cons_to_append >cons_to_append in ⊢ (???%);
+                                       >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%);
+                                       @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
+                                  | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
+                                  ]
+                              ]
+                        ]
+                    ]
+             ]
+      ]
+] qed.             
+                                                        
+lemma lset_inclusion_difference :
+  ∀A : DeqSet.
+  ∀s1,s2 : lset (carr A).
+    lset_inclusion ? s1 s2 →
+    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
+          lset_disjoint ? s1 s2' ∧
+          lset_eq ? s2' (lset_difference ? s2 s1).
+#A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj
+[ 1: @lset_inclusion_difference_aux @Hincl
+| 2: /2 by lset_difference_disjoint/
+| 3,4: @reflexive_lset_inclusion ]
+qed.
+
+          
+lemma memory_eq_to_memory_ext_pre :
+  ∀m1,m1',m2,writeable.
+  memory_eq m1 m1' →
+  sr_memext m1' m2 writeable →
+  sr_memext m1 m2 writeable.
+#m1 #m1' #m2 #writeable #Heq #Hext
+lapply (memory_eq_to_mem_ext … Heq) #Hext'
+@(memory_ext_transitive … Hext' Hext)
+qed.
+
+lemma memory_eq_to_memory_ext_post :
+  ∀m1,m2,m2',writeable.
+  memory_eq m2' m2 →
+  sr_memext m1 m2' writeable →
+  sr_memext m1 m2 writeable.
+#m1 #m2 #m2' #writeable #Heq #Hext
+lapply (memory_eq_to_mem_ext … Heq) #Hext'
+lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
+qed.
+
 
 lemma memext_free_extended_environment :
@@ -2158 +2166 @@
 ] qed.
 
+(* --------------------------------------------------------------------------- *)
+(* Some lemmas allowing to reason on writes to extended memories. *)
+
+(* Writing in the extended part of the memory preserves the extension (that's the point) *)
+lemma bestorev_writeable_memory_ext :
+  ∀m1,m2,writeable.
+  ∀Hext:sr_memext m1 m2 writeable.
+  ∀wb,wo,v. meml ? wb writeable →
+  ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' →
+  sr_memext m1 m2' writeable.
+#m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2'
+whd in ⊢ ((??%?) → ?);
+lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt
+>(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H
+lapply (if_opt_inversion ???? H) -H * #Hzltb
+lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb
+#Heq destruct %
+[ 1: #b #Hnonempty1
+     lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b
+     #Heq @conj
+     [ 1: % whd whd in Hvalid_b; try @Hvalid_b
+          normalize cases (block_region b) normalize nodelta
+          cases (block_region wb) normalize nodelta try //
+          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
+          try //
+     | 2: whd in ⊢ (??%%);
+          @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb
+          lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb)
+          * #H @(False_ind … (H Hmem)) ]
+| 2: #b #Hmem_writeable
+     lapply (me_writeable_valid … Hext … Hmem_writeable) #H %
+     [ 1: normalize cases H //
+     | 2: cases H normalize #Hb_lt #Hb_nonempty2
+          cases (block_region b)
+          cases (block_region wb) normalize nodelta
+          //
+          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
+          // ]
+| 3: #b #Hnonempty
+     lapply (me_not_writeable … Hext … Hnonempty) //
+] qed.
+
+(* If we manage to write in a block, then it is nonempty *)
+lemma bestorev_success_nonempty :
+  ∀m,wb,wo,v,m'.
+  bestorev m (mk_pointer wb wo) v = Some ? m' →
+  nonempty_block m wb.
+#m #wb #wo #v #m' normalize #Hstore
+cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H
+cases (if_opt_inversion ???? H) -H #nonempty #H %
+[ 1: whd @Zltb_true_to_Zlt assumption
+| 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H'
+     cut (Zleb (low (blocks m wb)) z = true)
+     [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ]
+     #Hleb >Hleb in H'; normalize nodelta #Hlt
+     lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt)
+     /2 by Zle_to_Zlt_to_Zlt/
+] qed.
+
+(* If we manage to write in a block, it is still non-empty after the write *)
+lemma bestorev_success_nonempty2 :
+  ∀m,wb,wo,v,m'.
+  bestorev m (mk_pointer wb wo) v = Some ? m' →
+  nonempty_block m' wb.
+#m #wb #wo #v #m' normalize #Hstore
+cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H
+cases (if_opt_inversion ???? H) -H #nonempty #H %
+[ 1: whd destruct @Zltb_true_to_Zlt assumption
+| 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H'
+     cut (Zleb (low (blocks m wb)) z = true)
+     [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ]
+     #Hleb >Hleb in H'; normalize nodelta #Hlt
+     lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt)
+     destruct cases (block_region wb) normalize >eqZb_z_z normalize
+     /2 by Zle_to_Zlt_to_Zlt/
+] qed.
+
+(* A nonempty block stays nonempty after a write. *)
+lemma nonempty_block_update_ok :
+  ∀m,b,wb,offset,v.
+  nonempty_block m b →
+  nonempty_block
+    (mk_mem
+      (update_block ? wb
+        (mk_block_contents (low (blocks m wb)) (high (blocks m wb))
+          (update beval offset v (contents (blocks m wb)))) (blocks m))
+            (nextblock m) (nextblock_pos m)) b.
+#m #b #wb #offset #v * #Hvalid #Hnonempty % //
+cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
+cases br normalize nodelta cases wbr normalize nodelta //
+@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
+qed.
+
+lemma nonempty_block_update_ok2 :
+  ∀m,b,wb,offset,v.
+  nonempty_block
+    (mk_mem
+      (update_block ? wb
+        (mk_block_contents (low (blocks m wb)) (high (blocks m wb))
+          (update beval offset v (contents (blocks m wb)))) (blocks m))
+            (nextblock m) (nextblock_pos m)) b →
+  nonempty_block m b.
+#m #b #wb #offset #v * #Hvalid #Hnonempty % //
+cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
+cases br normalize nodelta cases wbr normalize nodelta //
+@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
+qed.
+
+(* Writing in the non-extended part of the memory preserves the extension as long
+ * as it's done identically in both memories. *)
+lemma bestorev_not_writeable_memory_ext :
+  ∀m1,m2,writeable.
+  ∀Hext:sr_memext m1 m2 writeable.
+  ∀wb,wo,v.
+  ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' →  
+  ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧
+        sr_memext m1' m2' writeable.
+#m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1
+lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty
+cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq
+cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2')
+[ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize
+  normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
+  whd in Hstore1:(??%%); normalize
+  cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H
+  cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H
+  cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 
+  >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1
+  normalize nodelta /2 by ex_intro/ ]
+* #m2' #Hstore2 %{m2'} @conj try assumption
+whd in Hstore1:(??%%);
+whd in Hstore2:(??%%);
+cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H
+cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H
+cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H
+cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H
+cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1
+cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2
+cut (valid_pointer m1 (mk_pointer wb wo))
+[ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta
+     >Hltb1 @I ]
+#Hvalid
+lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable
+destruct %
+[ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB
+     @conj
+     [ 1: @nonempty_block_update_ok //
+     | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid
+          cases br cases wbr normalize nodelta
+          @(eqZb_elim … bid wbid) normalize nodelta //
+          #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ]
+| 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok
+| 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty)
+     @(me_not_writeable … Hext)
+] qed.
+
+(* If we successfuly store something in the first memory, then we can store it in the
+ * second one and the memory extension is preserved. *)
+lemma memext_store_value_of_type : 
+       ∀m, m_ext, m', writeable, ty, loc, off, v.
+       sr_memext m m_ext writeable →
+       store_value_of_type ty m loc off v = Some ? m' →
+       ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧
+                sr_memext m' m_ext' writeable.
+#m #m_ext #m' #writeable #ty #loc #off #v #Hext
+(* case analysis on access mode of [ty] *)
+cases ty
+[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
+whd in ⊢ ((??%?) → (?%?));
+[ 1,5,6,7,8: #Habsurd destruct ]
+whd in ⊢ (? → (??(λ_.?(??%?)?)));
+lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m'
+elim (fe_to_be_values ??)
+[ 1,3,5,7: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize //
+| 2,4,6,8: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H
+           cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq
+           lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq)
+           * #m_ext'' * #Hstore_eq2 #Hext2
+           lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' *
+           #Hstoren' #Hext3
+           %{m_ext'} @conj try assumption
+           whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta
+           @Hstoren'
+] qed.
+
+lemma memext_store_value_of_type' : 
+       ∀m, m_ext, m', writeable, ty, ptr, v.
+       sr_memext m m_ext writeable →
+       store_value_of_type' ty m ptr v = Some ? m' →
+       ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧
+                sr_memext m' m_ext' writeable.
+#m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o
+@memext_store_value_of_type @Hext qed.
 
 (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
@@ -2186 +2388 @@
 
 (* Simulation relations. *)
-inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
-| swc_stop : ∀fvs.
-    switch_cont_sim fvs Kstop Kstop
-| swc_seq : ∀fvs,s,k,k',u,result.
+inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝
+| swc_stop :
+    ∀new_vars. switch_cont_sim new_vars Kstop Kstop
+| swc_seq : ∀s,k,k',u,s',new_vars.
     fresh_for_statement s u →
-    switch_cont_sim fvs k k' →
-    switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
-| swc_while : ∀fvs,e,s,k,k',u,result.
+    switch_cont_sim new_vars k k' →
+    s' = ret_st ? (switch_removal s u) →
+    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →
+    switch_cont_sim new_vars (Kseq s k) (Kseq s' k')
+| swc_while : ∀e,s,k,k',u,s',new_vars.
     fresh_for_statement (Swhile e s) u →
-    switch_cont_sim fvs k k' →
-    switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
-| swc_dowhile : ∀fvs,e,s,k,k',u,result.
+    switch_cont_sim new_vars k k' →
+    s' = ret_st ? (switch_removal s u) →    
+    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →    
+    switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k')
+| swc_dowhile : ∀e,s,k,k',u,s',new_vars.
     fresh_for_statement (Sdowhile e s) u →
-    switch_cont_sim fvs k k' →
-    switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
-| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
+    switch_cont_sim new_vars k k' →
+    s' = ret_st ? (switch_removal s u) →        
+    lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars →    
+    switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k')
+| swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars.
     fresh_for_statement (Sfor Sskip e s1 s2) u →
-    switch_cont_sim fvs k k' →
-    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
-    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
-| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
+    switch_cont_sim new_vars k k' →
+    s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) →
+    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →    
+    switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k')
+| swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars.
     fresh_for_statement (Sfor Sskip e s1 s2) u →
-    switch_cont_sim fvs k k' →
-    switch_removal s1 fvs u = Some ? result1 →
-    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
-    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
-| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
+    switch_cont_sim new_vars k k' →
+    result1 = ret_st ? (switch_removal s1 u) →
+    result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) →
+    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →
+    switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k')
+| swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars.
     fresh_for_statement (Sfor Sskip e s1 s2) u →
-    switch_cont_sim fvs k k' →
-    switch_removal s1 fvs u = Some ? result1 →
-    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
-    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
-| swc_switch : ∀fvs,k,k'.
-    switch_cont_sim fvs k k' → 
-    switch_cont_sim fvs (Kswitch k) (Kswitch k')
-| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
-    switch_cont_sim fvs k k' →
-    (* /!\ Update [en] with [fvs'] ... *)
-    switch_cont_sim 
-      (map … (fst ??) (\snd (function_switch_removal f)))
+    switch_cont_sim new_vars k k' →
+    result1 = ret_st ? (switch_removal s1 u) →
+    result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) →
+    lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars →
+    switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k')
+| swc_switch : ∀k,k',new_vars.
+    switch_cont_sim new_vars k k' →
+    switch_cont_sim new_vars (Kswitch k) (Kswitch k')
+| swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *)       
+    switch_cont_sim old_vars k k' →
+    old_vars = \snd (function_switch_removal f) →
+    disjoint_extension en en' old_vars →
+    switch_cont_sim
+      new_vars
       (Kcall r f en k)
       (Kcall r (\fst (function_switch_removal f)) en' k').
-
-(* 
- en' = exec_alloc_variables en m (\snd (function_switch_removal f))
- TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
-        variable dans en'. 
-
-        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que 
-           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
-           de savoir que :
-           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
-           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
-           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
-           et à etre "(function_switch_removal f)-contained".
-
-        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
-           et l'update n'altèrent pas le comportement du reste du programme.
-
-        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
-                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
-                   en particulier, si u est frais pour S1 u est frais pour S0.
-
-        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
-                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
-                    
- ---------------------------------------------------------------
- . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
-   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
-   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
-   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
-*)
 
 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
@@ -2277 +2456 @@
  (* current statement *)
  ∀sss_statement  : statement.
- (* statement after transformation *)
- ∀sss_result     : swret statement.
  (* label universe *)
  ∀sss_lu         : universe SymbolTag.
@@ -2309 +2486 @@
  (* The extended environment does not interfer with the old one. *)
  ∀sss_env_hyp    : disjoint_extension sss_env sss_env_ext sss_new_vars.
+ (* Extension blocks are writeable. *)
+ ∀sss_ext_write  : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable.
  (* conversion of the current statement, using the variables produced during the conversion of the current function *)
- ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result.
+ ∀sss_result_rec.
+ ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec.
+ ∀sss_result.
+ sss_result = ret_st ? sss_result_rec →
+ (* inclusion of the locally produced new variables in the global new variables *)
+ lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars →
  (* simulation between the continuations before and after conversion. *)
- ∀sss_k_hyp      : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext.  
+ ∀sss_k_hyp      : switch_cont_sim sss_new_vars sss_k sss_k_ext.
  ext_fresh_for_genv sss_new_vars ge →
     switch_state_sim
       ge
       (State sss_func sss_statement sss_k sss_env sss_m)
-      (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext)
-| sws_callstate : ∀vars, fd,args,k,k',m.
-    switch_cont_sim vars k k' →
-    switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 
-| sws_returnstate : 
- ∀ssr_vars.
+      (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext)
+| sws_callstate :
+ ∀ssc_fd.
+ ∀ssc_args.
+ ∀ssc_k.
+ ∀ssc_k_ext.
+ ∀ssc_m.
+ ∀ssc_m_ext.
+ ∀ssc_writeable.
+ ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable.
+ (match ssc_fd with
+  [ CL_Internal ssc_f ⇒
+    switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
+  | _ ⇒ True ]) →
+    switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m)
+                        (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
+| sws_returnstate :
  ∀ssr_result.
  ∀ssr_k       : cont.
@@ -2330 +2525 @@
  ∀ssr_writeable : list block.
  ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable.
+ ∀ssr_vars.
     switch_cont_sim ssr_vars ssr_k ssr_k_ext →
     switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext)
@@ -2335 +2531 @@
     switch_state_sim ge (Finalstate r) (Finalstate r).
 
-lemma call_cont_swremoval : ∀fv,k,k'.
-  switch_cont_sim fv k k' →
-  switch_cont_sim fv (call_cont k) (call_cont k').
-#fv #k0 #k0' #K elim K /2/
+lemma call_cont_swremoval : ∀k,k',vars.
+  switch_cont_sim vars k k' →
+  switch_cont_sim vars (call_cont k) (call_cont k').
+#k0 #k0' #vars #K elim K /2/
 qed.
 
@@ -2444 +2640 @@
 qed.
 
-
-(* Conservation of the smenantics of binary operators under memory extensions *)
+(* Conservation of the semantics of binary operators under memory extensions.
+   Tried to factorise it a bit but the play with indexes just becomes too messy.  *)
 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable.
   ∀Hext:sr_memext m1 m2 writeable. ∀res.
@@ -2454 +2650 @@
 try //
 whd in match (sem_binary_operation ??????);
+lapply (me_valid_pointers … Hmemext)
+lapply (me_not_writeable_ptr … Hmemext)
 elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1
 elim m2 #contents2 #nextblocks2 #Hnextpos2
-* #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons
+* #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid
 whd in match (sem_cmp ??????);
 whd in match (sem_cmp ??????);
-[ 1: cases (classify_cmp (typeof e1) (typeof e2))
+[ 1,2: cases (classify_cmp (typeof e1) (typeof e2))
      normalize nodelta
-     [ 1: #sz #sg try //
-     | 2: #opt #ty
+     [ 1,5: #sz #sg try //
+     | 2,6: #opt #ty
           cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
+          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
           cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
+          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
+          lapply (Hvalid ptr)
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ]
-          #Hvalid >(Hvalid (refl ??))
-          lapply (Hvalid_cons ptr')
+          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
+          #Hvalid' >(Hvalid' (refl ??))
+          lapply (Hvalid ptr')
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
-| 2: cases (classify_cmp (typeof e1) (typeof e2))
+          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
+          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
+     | 3,7: #fsz #H @H
+     | 4,8: #ty1 #ty2 #H @H ]
+| 3,4: cases (classify_cmp (typeof e1) (typeof e2))
      normalize nodelta
-     [ 1: #sz #sg try //
-     | 2: #opt #ty
+     [ 1,5: #sz #sg try //
+     | 2,6: #opt #ty
           cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
+          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
           cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
+          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
+          lapply (Hvalid ptr)
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H >(H (refl ??))
-          lapply (Hvalid_cons ptr')
+          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
+          #Hvalid' >(Hvalid' (refl ??))
+          lapply (Hvalid ptr')
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) #Hok @Hok
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
-| 3: cases (classify_cmp (typeof e1) (typeof e2))
+          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
+          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
+     | 3,7: #fsz #H @H
+     | 4,8: #ty1 #ty2 #H @H ]
+| 5,6: cases (classify_cmp (typeof e1) (typeof e2))
      normalize nodelta
-     [ 1: #sz #sg try //
-     | 2: #opt #ty
+     [ 1,5: #sz #sg try //
+     | 2,6: #opt #ty
           cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
+          [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
           cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
+          [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
+          [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
+          | 7,8: #H @H ]
+          lapply (Hvalid ptr)
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H >(H (refl ??))
-          lapply (Hvalid_cons ptr')
+          [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ]
+          #Hvalid' >(Hvalid' (refl ??))
+          lapply (Hvalid ptr')
           cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) #Hok @Hok
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
-| 4: cases (classify_cmp (typeof e1) (typeof e2))
-     normalize nodelta
-     [ 1: #sz #sg #H @H          
-     | 2: #opt #ty
-          cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H >(H (refl ??))
-          lapply (Hvalid_cons ptr')
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) #Hok @Hok
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
-| 5: cases (classify_cmp (typeof e1) (typeof e2))
-     normalize nodelta
-     [ 1: #sz #sg #H @H          
-     | 2: #opt #ty
-          cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H >(H (refl ??))
-          lapply (Hvalid_cons ptr')
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) #Hok @Hok
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
-| 6: cases (classify_cmp (typeof e1) (typeof e2))
-     normalize nodelta
-     [ 1: #sz #sg #H @H          
-     | 2: #opt #ty
-          cases v1 normalize nodelta
-          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          cases v2 normalize nodelta
-          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
-          [ 1,2,3: #Habsurd destruct (Habsurd)
-          | 4: #H @H ]
-          lapply (Hvalid_cons ptr)
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H >(H (refl ??))
-          lapply (Hvalid_cons ptr')
-          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
-          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
-          #H' >(H' (refl ??)) #Hok @Hok
-     | 3: #fsz #H @H
-     | 4: #ty1 #ty2 #H @H ]
+          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
+          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
+     | 3,7: #fsz #H @H
+     | 4,8: #ty1 #ty2 #H @H ]
 ] qed.
 
@@ -2749 +2881 @@
 ] qed.
 
+lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext.
+  (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty)
+                           (exec_lvalue' ge' env_ext m_ext ed ty)) →
+  ∀e. exec_lvalue_sim (exec_lvalue ge env m e)
+                      (exec_lvalue ge' env_ext m_ext e).
+#ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed.
+
+lemma exec_expr_sim_to_exec_exprlist :
+  ∀ge,ge',en1,en2,m1,m2.
+  (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) →
+   ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l).
+#ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l
+[ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl
+| 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?));
+     lapply (Hsim hd)
+     cases (exec_expr ge en1 m1 hd)
+     [ 2: #error normalize #_ #Habsurd destruct (Habsurd)
+     | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??))
+          normalize nodelta 
+          cases (exec_exprlist ge en1 m1 tl) in Hind;
+          [ 2: #error normalize #_ #Habsurd destruct (Habsurd)
+          | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl
+          ]
+     ]
+] qed.
+
 (*
 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
@@ -2776 +2934 @@
 (* The return type of any function is invariant under switch removal *)
 lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
-#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
+#f elim f #ty #args #vars #body whd in match (function_switch_removal ?);
+cases (switch_removal ??) * #stmt #fvs #u @refl
 qed.
 
 (* Similar stuff for fundefs *)
 lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
-* // qed.
+* // * #ty #args #vars #body whd in ⊢ (??%%);
+whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u
+normalize nodelta #u @refl
+qed.
 
 (*
@@ -2820 +2982 @@
 cases (leb e s) try /2/
 qed.
+
 (*
 lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
@@ -2861 +3024 @@
 qed.*)
 
-(*
-lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
+lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf.
 *
-[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
-| 2: #e1 #e2 #u #_ 
-     whd in match (sw_rem ??);
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 3: #ret #f #args #u
-     whd in match (sw_rem ??);
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 4: #s1 #s2 #u
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);     
-     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
-     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 5: #e #s1 #s2 #u #_
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);     
-     cases (switch_removal ? ?) * #a #b #c normalize nodelta
-     cases (switch_removal ? ?) * #e #f #h normalize nodelta
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 6,7: #e #s #u #_
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);     
-     cases (switch_removal ? ?) * #a #b #c normalize nodelta
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 8: #s1 #e #s2 #s3 #u #_     
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);     
+[ 1: * #H @(False_ind … (H (refl ??))) ]
+try /2/
+[ 1: #s1 #s2 #_ #u normalize 
      cases (switch_removal ? ?) * #a #b #c normalize nodelta
      cases (switch_removal ? ?) * #e #f #g normalize nodelta
-     cases (switch_removal ? ?) * #i #j #k normalize nodelta
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 9,10: #u #_     
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 11: #e #u #_
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 12: #e #ls #u #_
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);
+     /2 by ex_intro/
+| 2: #e #s1 #s2 #_ #u normalize
+     cases (switch_removal ? ?) * #a #b #c normalize nodelta
+     cases (switch_removal ? ?) * #e #f #g normalize nodelta
+     /2 by ex_intro/
+| 3,4: #e #s #_ #u normalize
+     cases (switch_removal ? ?) * #e #f #g normalize nodelta
+     /2 by ex_intro/
+| 5: #s1 #e #s2 #s3 #_ #u normalize     
+     cases (switch_removal ? ?) * #a #b #c normalize nodelta
+     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
+     cases (switch_removal ? ?) * #h #i #j normalize nodelta
+     /2 by ex_intro/
+| 6: #e #ls #_ #u normalize
      cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
      cases (fresh ??) #e #f normalize nodelta
-     normalize in match (simplify_switch ???);
      cases (fresh ? f) #g #h normalize nodelta
      cases (produce_cond ????) * #k #l #m normalize nodelta
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 13,15: #lab #st #u #_
-     whd in match (sw_rem ??);
-     whd in match (switch_removal ??);
-     cases (switch_removal ? ?) * #a #b #c normalize nodelta
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/
-| 14: #lab #u     
-     whd in match (is_Sskip ?);
-     try /2 by refl, ex_intro/ ]
-qed.
-*)
+     /2 by ex_intro/
+| 7,8: #ls #st #_ #u normalize
+     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
+     /2 by ex_intro/
+] qed.
 
 (*
@@ -2989 +3115 @@
 ] qed.
 
-lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
-
-lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
-#A #B #a #b * #a' #b' #H destruct @refl
-qed.
-
-lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
-#A #B #a #b * #a' #b' #H destruct @refl
-qed.
+lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉.
+#s #u cases (switch_removal s u) * #s' #fvs' #u'
+%{s'} %{fvs'} %{u'} @refl
+qed.
+
+lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉.
+#ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed.
+
+lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
+
+lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉.
+#e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed.
+
+(* ---------------------------------------------------------------------------- 
+   What follows is some rather generic stuff on proving that reading where we  
+   just wrote yields what we expect. We have to prove everything at the back-end
+   level, and then lift this to the front-end. This entails having to reason on
+   invariants bearing on "intervals" of memories, and a lot of annoying stuff
+   to go back and forth nats, Zs and bitvectors ... *)
+
+lemma fold_left_neq_acc_neq : 
+  ∀m. ∀acc1,acc2. ∀y1,y2:BitVector m.
+    acc1 ≠ acc2 → 
+    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc1 y1 ≠
+    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc2 y2.
+#m elim m
+[ 1: #acc1 #acc2 #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
+| 2: #m' #Hind #acc1 #acc2 #y1 #y2
+     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
+     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
+     >Heq1 >Heq2 * #Hneq % whd in ⊢ ((??%%) → ?);
+     cases hd1 cases hd2 normalize nodelta #H
+     [ 1: lapply (Hind (p1 acc1) (p1 acc2) tl1 tl2 ?)
+          [ 1: % #H' @Hneq destruct (H') @refl ] 
+          * #H' @H' @H
+     | 4: lapply (Hind (p0 acc1) (p0 acc2) tl1 tl2 ?)
+          [ 1: % #H' @Hneq destruct (H') @refl ] 
+          * #H' @H' @H
+     | 2: lapply (Hind (p1 acc1) (p0 acc2) tl1 tl2 ?)
+          [ 1: % #H' destruct ]
+          * #H' @H' try @H
+     | 3: lapply (Hind (p0 acc1) (p1 acc2) tl1 tl2 ?)
+          [ 1: % #H' destruct ]
+          * #H' @H' try @H ]
+] qed.          
+
+lemma fold_left_eq :
+  ∀m. ∀acc. ∀y1,y2:BitVector m.
+    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y1 =
+    fold_left Pos bool m (λacc:Pos.λb:bool.if b then p1 acc else p0 acc) acc y2 →
+    y1 = y2.
+#m elim m
+[ 1: #acc #y1 #y2 >(BitVector_O … y1) >(BitVector_O … y2) //
+| 2: #m' #Hind #acc #y1 #y2
+     elim (BitVector_Sn … y1) #hd1 * #tl1 #Heq1
+     elim (BitVector_Sn … y2) #hd2 * #tl2 #Heq2
+     >Heq1 >Heq2 whd in ⊢ ((??%%) → ?);
+     cases hd1 cases hd2 normalize nodelta
+     [ 1,4: #H >(Hind … H) @refl
+     | 2: #Habsurd lapply (fold_left_neq_acc_neq ? (p1 acc) (p0 acc) tl1 tl2 ?)
+          [ 1: % #H' destruct ]
+          * #H @(False_ind … (H Habsurd))
+     | 3: #Habsurd lapply (fold_left_neq_acc_neq ? (p0 acc) (p1 acc) tl1 tl2 ?)
+          [ 1: % #H' destruct ]
+          * #H @(False_ind … (H Habsurd)) ]
+] qed.
+
+lemma bv_neq_Z_neq_aux : 
+  ∀n. ∀bv1,bv2 : BitVector n. ∀f.
+    Z_of_unsigned_bitvector n bv1 ≠ 
+    pos (fold_left Pos bool n (λacc:Pos.λb:bool.if b then p1 acc else p0 acc ) (f one) bv2).
+#n elim n
+[ 1: #bv1 #bv2 >(BitVector_O … bv1) >(BitVector_O … bv2) #f normalize % #H destruct
+| 2: #n' #Hind #bv1 #bv2 #f
+     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
+     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
+     >Heq1 >Heq2 %
+     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
+     cases hd1 cases hd2 normalize nodelta
+     normalize in ⊢ ((??%%) → ?);
+     [ 1: #Hpos destruct (Hpos)
+          lapply (fold_left_neq_acc_neq ? one (p1 (f one)) tl1 tl2 ?)
+          [ 1: % #H destruct ]
+          * #H @H @e0
+     | 2: #Hpos destruct (Hpos)
+          lapply (fold_left_neq_acc_neq ? one (p0 (f one)) tl1 tl2 ?)
+          [ 1: % #H destruct ]
+          * #H @H @e0
+     | 3: #H cases (Hind tl1 tl2 (λx. p1 (f x))) #H' @H' @H
+     | 4: #H cases (Hind tl1 tl2 (λx. p0 (f x))) #H' @H' @H
+     ]
+] qed.     
+
+lemma bv_neq_Z_neq : ∀n. ∀bv1,bv2: BitVector n. 
+  bv1 ≠ bv2 → Z_of_unsigned_bitvector n bv1 ≠ Z_of_unsigned_bitvector n bv2.
+#n #bv1 #bv2 * #Hneq % #Hneq' @Hneq -Hneq lapply Hneq' -Hneq'
+lapply bv2 lapply bv1 -bv1 -bv2
+elim n
+[ 1: #bv1 #bv2 >(BitVector_O bv1) >(BitVector_O bv2) //
+| 2: #n' #Hind #bv1 #bv2
+     elim (BitVector_Sn … bv1) #hd1 * #tl1 #Heq1
+     elim (BitVector_Sn … bv2) #hd2 * #tl2 #Heq2
+     >Heq1 >Heq2
+     whd in match (Z_of_unsigned_bitvector ??) in ⊢ ((??%%) → ?);
+     cases hd1 cases hd2 normalize nodelta
+     [ 1: #Heq destruct (Heq) lapply (fold_left_eq … e0) * @refl
+     | 4: #H >(Hind ?? H) @refl
+     | 2: #H lapply (sym_eq ??? H) -H #H
+          cases (bv_neq_Z_neq_aux ? tl2 tl1 (λx.x)) #H' @(False_ind … (H' H))
+     | 3: #H
+          cases (bv_neq_Z_neq_aux ? tl1 tl2 (λx.x)) #H' @(False_ind … (H' H)) ]
+] qed.
+
+definition Z_of_offset ≝ λofs.Z_of_unsigned_bitvector ? (offv ofs).
+
+(* This axiom looks reasonable to me. But I slept 3 hours last night. *)
+axiom bv_incr_to_Z : ∀sz.∀bv:BitVector sz. 
+  Z_of_unsigned_bitvector ? (increment ? bv) = OZ ∨
+  Z_of_unsigned_bitvector ? (increment ? bv) = (Zsucc (Z_of_unsigned_bitvector ? bv)).
+                                            
+(* Note the possibility of overflow of bv. But it should be allright in the big picture. *)
+lemma offset_succ_to_Z_succ :
+  ∀bv : BitVector 16. ∀x. Z_of_unsigned_bitvector ? bv < x → Z_of_unsigned_bitvector ? (increment ? bv) ≤ x.
+#bv #x
+cases (bv_incr_to_Z ? bv)
+[ 1: #Heq >Heq lapply (Z_of_unsigned_not_neg bv) *
+     [ 1: #Heq >Heq elim x //
+     | 2: * #p #H >H elim x // ]
+| 2: #H >H elim x
+     elim (Z_of_unsigned_bitvector 16 bv) try /2/
+] qed.
+
+(*
+lemma Z_not_le_shifted : ∀ofs.
+  (Z_of_unsigned_bitvector 16 (offv (shift_offset 2 ofs (bitvector_of_nat 2 1))) ≤ Z_of_unsigned_bitvector 16 (offv ofs)) → False.
+* #vec *)
+
+(* We prove the following properties for bestorev :
+  1) storing doesn't modify the nextblock
+  2) it does not modify the extents of the block written to
+  3) since we succeeded in storing, the offset is in the bounds
+  4) reading where we wrote yields the obvious result
+  5) besides the written offset, the memory contains the same stuff
+*)
+lemma mem_bounds_invariant_after_bestorev :
+∀m,m',b,ofs,bev.
+  bestorev m (mk_pointer b ofs) bev = Some ? m' →
+  nextblock m' = nextblock m ∧
+  (∀b.low (blocks m' b) = low (blocks m b) ∧
+      high (blocks m' b) = high (blocks m b)) ∧
+  (low (blocks m b) ≤ (Z_of_offset ofs) ∧
+   (Z_of_offset ofs) < high (blocks m b)) ∧   
+  (contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv ofs)) = bev) ∧
+  (∀o. o ≠ ofs → contents (blocks m' b) (Z_of_unsigned_bitvector ? (offv o)) = 
+                 contents (blocks m b) (Z_of_unsigned_bitvector ? (offv o))).
+#m #m' #b #ofs #bev whd in ⊢ ((??%?) → ?);
+#H
+cases (if_opt_inversion ???? H) #Hlt -H normalize nodelta #H
+cases (if_opt_inversion ???? H) #Hlelt -H #H
+cases (andb_inversion … Hlelt) #Hle #Hlt @conj try @conj try @conj try @conj
+destruct try @refl
+[ 1:
+  #b' normalize cases b #br #bid cases b' #br' #bid'
+  cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
+  try /2 by conj, refl/
+| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
+| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
+| 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
+     >eqZb_z_z @refl
+| 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
+     >eqZb_z_z normalize nodelta
+     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
+     [ 1,3: lapply Hneq cases o #bv1 cases ofs #bv2
+            #Hneq lapply (bv_neq_Z_neq ? bv1 bv2 ?)
+            [ 1,3: % #Heq destruct cases Hneq #H @H @refl ]
+            * #H #Habsurd @(False_ind … (H Habsurd))
+     | 2,4: normalize nodelta #H @refl ]
+] qed.
+
+(* Shifts an offset [i] times. storen uses a similar operation internally. *)
+let rec shiftn (off:offset) (i:nat) on i : offset ≝
+match i with
+[ O ⇒ off
+| S n ⇒
+  shiftn (shift_offset 2 off (bitvector_of_nat … 1)) n
+].
+
+(* This axioms states that if we do not stray too far, we cannot circle back to ourselves. Pretty trivial, but a
+   serious PITA to prove. *)
+axiom shiftn_no_wrap : ∀i. i ≤ 8 → ∀ofs. shiftn ofs i ≠ ofs.
+
+(* We prove some properties of [storen m ptr data]. Note that [data] is a list of back-end chunks.
+   What we expect [storen] to do is to store this list starting at [ptr]. The property we expect to
+   have is that the contents of this particular zone (ptr to ptr+|data|-1) match exactly [data], and
+   that elsewhere the memory is untouched.
+   Not so simple. Some observations:
+   A) Pointers are encoded as block+offsets, and offsets are bitvectors, hence limited in range (2^16).
+      On the other hand, block extents are encoded on Zs and are unbounded. This entails some problems
+      when writing at the edge of the range of offsets and wrapping around, but that can be solved 
+      resorting to ugliness and trickery.
+   B) The [data] list is unbounded. Taking into account the point A), this means that we can lose
+      data when writing (exactly as when we write in a circular buffer, overwriting previous stuff).
+      The only solution to that is to explicitly bound |data| with something reasonable.
+   Taking these observations into account, we prove the following invariants:
+  1) storing doesn't modify the nextblock (trivial)
+  2) it does not modify the extents of the block written to (trivial)
+  3) all the offsets on which we run while writing are legal (trivial)
+  3) if we index properly, we hit the stored data in the same order as in the list
+  4) If we hit elsewhere, we find the memory unmodified. We have a problem for defining "elsewhere",
+     because bitvectors (hence offsets) are limited in their range. For now, we define "elsewhere" as 
+     "not reachable by shiftn from [ofs] to |data|"
+  5) the pointer we write to is valid (trivial)
+*)
+lemma mem_bounds_invariant_after_storen :
+  ∀data,m,m',b,ofs.
+    |data| ≤ 8 → (* 8 is the size of a double. *)
+    storen m (mk_pointer b ofs) data = Some ? m' →
+    (nextblock m' = nextblock m ∧
+    (∀b.low (blocks m' b) = low (blocks m b) ∧
+        high (blocks m' b) = high (blocks m b)) ∧
+    (∀index. index < |data| → low (blocks m b) ≤ (Z_of_offset (shiftn ofs index)) ∧
+                               Z_of_offset (shiftn ofs index) < high (blocks m b)) ∧
+    (∀index. index < |data| → nth_opt ? index data = Some ? (contents (blocks m' b) (Z_of_offset (shiftn ofs index)))) ∧
+    (∀o. (∀i. i < |data| → o ≠ shiftn ofs i) →
+         contents (blocks m' b) (Z_of_offset o) = contents (blocks m b) (Z_of_offset o)) ∧
+    (|data| > 0 → valid_pointer m (mk_pointer b ofs) = true)).
+#l elim l
+[ 1: #m #m' #b #ofs #_ normalize #H destruct @conj try @conj try @conj try @conj try @conj try @refl
+     [ 1: #b0 @conj try @refl
+(*     | 2: #Habsurd @False_ind /2 by le_S_O_absurd/*)
+     | 2,3: #i #Habsurd @False_ind elim i in Habsurd; try /2/
+     | 4: #o #Hout @refl
+     | 5: #H @False_ind /2 by le_S_O_absurd/ ]
+| 2: #hd #tl #Hind #m #m' #b #ofs #Hsize_bound #Hstoren
+     whd in Hstoren:(??%?);
+     cases (some_inversion ????? Hstoren) #m'' * #Hbestorev -Hstoren #Hstoren
+     lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * #HA #HB #HI #HJ #HK
+     lapply (Hind … Hstoren) [ 1: /2 by le_S_to_le/ ] * * * * * 
+     #HC #HD #HE #HF #HV #HW @conj try @conj try @conj try @conj try @conj
+     [ 1: <HA <HC @refl
+     | 2: #b elim (HB b) #HF #HG elim (HD b) #HG #HH @conj try //     
+     | 4: *
+          [ 1: #_ <HJ whd in match (nth 0 ???);
+               lapply (HV ofs ?)
+               [ 1: #i #Hlt @sym_neq % #Heq lapply (shiftn_no_wrap (S i) ? ofs)
+                    [ 1: normalize in Hsize_bound;
+                         cut (|tl| < 8) [ /2 by lt_plus_to_minus_r/ ]
+                         #Hlt' lapply (transitive_lt … Hlt Hlt') // ]
+                    * #H @H whd in match (shiftn ??); @Heq
+               | 2: cases ofs #ofs' normalize // ]
+          | 2: #i' #Hlt lapply (HF i' ?)
+               [ 1: normalize normalize in Hlt; lapply (monotonic_pred … Hlt) //
+               | 2: #H whd in match (nth_opt ???); >H @refl ] ]
+     | 5: #o #H >HV
+          [ 2: #i #Hlt @(H (S i) ?) 
+               normalize normalize in Hlt; /2 by le_S_S/
+          | 1: @HK @(H 0) // ]     
+     | 6: #_ @(bestorev_to_valid_pointer … Hbestorev)
+     | 3: *
+          [ 1: #_ <HJ whd in match (shiftn ??);
+               lapply (Zleb_true_to_Zle (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
+               lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
+               whd in match (low_bound ??); whd in match (high_bound ??);
+               cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
+               cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs)))
+               [ 2: normalize #Habsurd destruct ] normalize nodelta #Hltb
+               lapply (Zltb_true_to_Zlt … Hltb) #Hlt' #Hleb lapply (Hleb (refl ??)) -Hleb #Hleb'
+               normalize @conj try assumption
+          | 2: #i' #Hlt cases (HB b) #Hlow1 #Hhigh1 cases (HD b) #Hlow2 #Hhigh2
+               lapply (HE i' ?) [ 1: normalize in Hlt ⊢ %;lapply (monotonic_pred … Hlt) // ]
+               >Hlow1 >Hhigh1 * #H1 #H2 @conj try @H1 try @H2
+          ]
+     ]
+] qed.
+
+lemma storen_beloadv_ok :
+  ∀m,m',b,ofs,hd,tl.
+  |hd::tl| ≤ 8 → (* 8 is the size of a double. *)
+  storen m (mk_pointer b ofs) (hd::tl) = Some ? m' →
+  ∀i. i < |hd::tl| → beloadv m' (mk_pointer b (shiftn ofs i)) = nth_opt ? i (hd::tl).
+#m #m' #b #ofs #hd #tl #Hle #Hstoren
+lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * * 
+#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
+#i #Hle lapply (Hdata i Hle) #Helt >Helt
+whd in match (beloadv ??); whd in match (nth_opt ???);
+lapply (Hvalid_ptr ?) try //
+whd in ⊢ ((??%?) → ?);
+>Hnext cases (Zltb (block_id b) (nextblock m))
+[ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct ]
+>andb_lsimpl_true normalize nodelta
+whd in match (low_bound ??); whd in match (high_bound ??);
+cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh #H
+lapply (Hvalid_offs i Hle) * #Hzle #Hzlt
+>(Zle_to_Zleb_true … Hzle) >(Zlt_to_Zltb_true … Hzlt) normalize nodelta @refl
+qed.
+
+lemma loadn_beloadv_ok :
+  ∀size,m,b,ofs,result.
+  loadn m (mk_pointer b ofs) size = Some ? result →
+  ∀i. i < size → beloadv m (mk_pointer b (shiftn ofs i)) = nth_opt ? i result.
+#size elim size
+[ 1: #m #b #ofs #result #Hloadn *
+     [ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
+     | 2: #i' #Habsurd @False_ind /2 by le_S_O_absurd/ ]
+| 2: #size' #Hind_size #m #b #ofs #result #Hloadn #i
+     elim i
+     [ 1: #_
+          cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
+          cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq
+          destruct (Heq) whd in match (shiftn ofs 0);
+          >Hbeloadv @refl
+    | 2: #i' #Hind #Hlt
+         whd in match (shiftn ofs (S i'));
+         lapply (Hind ?)
+         [ /2 by lt_S_to_lt/ ] #Hbeloadv_ind
+         whd in Hloadn:(??%?);
+         cases (some_inversion ????? Hloadn) #hd * #Hbeloadv #Hloadn'
+         cases (some_inversion ????? Hloadn') #tl * #Hloadn_tl #Heq -Hloadn'
+         destruct (Heq)
+         @Hind_size [ 2: lapply Hlt normalize @monotonic_pred ]
+         @Hloadn_tl
+    ]
+] qed.
+
+lemma storen_loadn_nonempty :
+  ∀data,m,m',b,ofs.
+  |data| ≤ 8 →
+  storen m (mk_pointer b ofs) data = Some ? m' →
+  ∃result. loadn m' (mk_pointer b ofs) (|data|) = Some ? result ∧ |result|=|data|.
+#data elim data
+[ 1: #m #m' #b #ofs #_ #Hstoren normalize in Hstoren; destruct %{[ ]} @conj try @refl ]
+#hd #tl #Hind #m #m' #b #ofs #Hle #Hstoren
+lapply (mem_bounds_invariant_after_storen … Hle Hstoren) * * * * *
+#Hnext #Hbounds #Hvalid_offs #Hdata #Hcontents_inv #Hvalid_ptr
+cases (some_inversion ????? Hstoren) #m0 * #Hbestorev #Hstoren0
+whd in match (loadn ???);
+lapply (bestorev_to_valid_pointer … Hbestorev) whd in ⊢ ((??%?) → ?);
+whd in match (beloadv ??);
+whd in match (low_bound ??); whd in match (high_bound ??);
+>Hnext
+cases (Zltb (block_id b) (nextblock m)) [ 2: normalize #Habsurd destruct ] >andb_lsimpl_true
+normalize nodelta cases (Hbounds b) #Hlow #Hhigh >Hlow >Hhigh
+cases (Zleb (low (blocks m b)) (Z_of_unsigned_bitvector offset_size (offv ofs))) normalize nodelta
+[ 2: #Habsurd destruct ] >andb_lsimpl_true
+#Hltb >Hltb normalize nodelta
+cases (Hind  … Hstoren0) [ 2: lapply Hle normalize /2 by le_S_to_le/ ]
+#tl' * #Hloadn >Hloadn #Htl' normalize nodelta
+%{(contents (blocks m' b) (Z_of_unsigned_bitvector offset_size (offv ofs))::tl')} @conj try @refl
+normalize >Htl' @refl
+qed.
+
+let rec double_list_ind 
+  (A : Type[0])
+  (P : list A → list A → Prop)
+  (base_nil  : P [ ] [ ])
+  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
+  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
+  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
+  (l1, l2 : list A) on l1 ≝
+match l1 with
+[ nil ⇒ 
+  match l2 with
+  [ nil ⇒ base_nil
+  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
+| cons hd1 tl1 ⇒  
+  match l2 with
+  [ nil ⇒ base_l1 hd1 tl1
+  | cons hd2 tl2 ⇒
+    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
+  ]
+].  
+
+lemma nth_eq_tl :
+  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
+  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) → 
+  (∀i. nth_opt A i l1 = nth_opt A i l2).
+#A #l1 #l2 @(double_list_ind … l1 l2)
+[ 1: #hd1 #hd2 #_ #i elim i try /2/
+| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
+| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
+| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
+     #Hind
+     @(λi. Hind (S i))
+] qed.     
+
+
+lemma nth_eq_to_eq :
+  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
+#A #l1 elim l1
+[ 1: #l2 #H lapply (H 0) normalize
+     cases l2
+     [ 1: //
+     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
+| 2: #hd1 #tl1 #Hind *
+     [ 1: #H lapply (H 0) normalize #Habsurd destruct
+     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
+          >(Hind tl2) try @refl @(nth_eq_tl … H)
+     ]
+] qed.
+
+(* for leb_elim, shadowed in positive.ma *)
+definition leb_elim' : ∀n,m:nat. ∀P:bool → Prop. 
+(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m) ≝ leb_elim.
+
+include alias "arithmetics/nat.ma".
+
+lemma nth_miss : ∀A:Type[0]. ∀l:list A. ∀i. |l| ≤ i → nth_opt A i l = None ?.
+#A #l elim l //
+#hd #tl #H #i elim i
+[ 1: normalize #Habsurd @False_ind /2 by le_S_O_absurd/
+| 2: #i' #H' #Hle whd in match (nth_opt ???); @H /2 by monotonic_pred/
+] qed.
+
+lemma storen_loadn_ok :
+  ∀data.
+  |data| ≤ 8 → (* 8 is the size of a double. *)
+  ∀m,m',b,ofs.
+  storen m (mk_pointer b ofs) data = Some ? m' →
+  loadn m' (mk_pointer b ofs) (|data|) = Some ? data.
+#data elim data try // #hd #tl #Hind #Hle #m #m' #b #ofs #Hstoren
+lapply (storen_beloadv_ok m m' …  Hle Hstoren) #Hyp_storen
+cases (storen_loadn_nonempty … Hle Hstoren) #result * #Hloadn #Hresult_sz
+lapply (loadn_beloadv_ok (|hd::tl|) m' b ofs … Hloadn) #Hyp_loadn
+cut (∀i. i < |hd::tl| → nth_opt ? i (hd::tl) = nth_opt ? i result)
+[ #i #Hlt lapply (Hyp_storen … i Hlt) #Heq1
+  lapply (Hyp_loadn … i Hlt) #Heq2 >Heq1 in Heq2; // ]
+#Hyp
+cut (result = hd :: tl)
+[ 2: #Heq destruct (Heq) @Hloadn ]
+@nth_eq_to_eq #i @sym_eq
+@(leb_elim' … (S i) (|hd::tl|))
+[ 1: #Hle @(Hyp ? Hle)
+| 2: #Hnle cut (|hd::tl| ≤ i)
+     [ lapply (not_le_to_lt … Hnle) normalize /2 by monotonic_pred/ ]
+     #Hle'
+     >nth_miss // >nth_miss //
+] qed.
+
+(* In order to prove the lemma on store_value_of_type and load_value_of_type,
+   we need to prove the fact that we store stuff of "reasonable" size, i.e. at most 8. *)
+lemma typesize_bounded : ∀ty. typesize ty ≤ 8.
+* try //
+[ 1: * try //
+| 2: * try //
+] qed.
+
+(* Lifting bound on make_list *)
+lemma makelist_bounded : ∀A,sz,bound,elt. sz ≤ bound → |make_list A elt sz| ≤ bound.
+#A #sz elim sz try //
+#sz' #Hind #bound #elt #Hbound normalize
+cases bound in Hbound;
+[ 1: #Habsurd @False_ind /2 by le_S_O_absurd/
+| 2: #bound' #Hbound' lapply (Hind bound' elt ?)
+     [ 1: /2 by monotonic_pred/
+     | 2: /2 by le_S_S/ ]
+] qed.
+
+lemma bytes_of_bitvector_bounded :
+  ∀sz,bv. |bytes_of_bitvector (size_intsize sz) bv| = size_intsize sz.
+* #bv normalize
+[ 1: cases (vsplit ????) normalize nodelta #bv0 #bv1 //
+| 2: cases (vsplit ????) normalize nodelta #bv0 #bv1
+     cases (vsplit ????) normalize nodelta #bv2 #bv3 //
+| 3: cases (vsplit ????) normalize nodelta #bv0 #bv1
+     cases (vsplit ????) normalize nodelta #bv2 #bv3
+     cases (vsplit ????) normalize nodelta #bv4 #bv5
+     cases (vsplit ????) normalize nodelta #bv6 #bv7
+     //
+] qed.
+
+lemma map_bounded :
+  ∀A,B:Type[0]. ∀l:list A. ∀f. |map A B f l| = |l|.
+  #A #B #l elim l try //
+qed.
+
+lemma fe_to_be_values_bounded : 
+  ∀ty,v. |fe_to_be_values ty v| ≤ 8.
+#ty cases ty
+[ 3: #fsz #v whd in match (fe_to_be_values ??);
+     cases v normalize nodelta
+     [ 1: @makelist_bounded @typesize_bounded
+     | 2: * normalize nodelta #bv
+          >map_bounded >bytes_of_bitvector_bounded //
+     | 3: #fl @makelist_bounded @typesize_bounded
+     | 4: //
+     | 5: #ptr // ]
+| 2: #v whd in match (fe_to_be_values ??);
+     cases v normalize nodelta
+     [ 1: @makelist_bounded @typesize_bounded
+     | 2: * normalize nodelta #bv
+          >map_bounded >bytes_of_bitvector_bounded //
+     | 3: #fl @makelist_bounded @typesize_bounded
+     | 4: //
+     | 5: #ptr // ]
+| 1: #sz #sg #v whd in match (fe_to_be_values ??);
+     cases v normalize nodelta
+     [ 1: @makelist_bounded @typesize_bounded
+     | 2: * normalize nodelta #bv
+          >map_bounded >bytes_of_bitvector_bounded //
+     | 3: #fl @makelist_bounded @typesize_bounded
+     | 4: //
+     | 5: #ptr // ]
+] qed.
+
+
+definition ast_typ_consistent_with_value : typ → val → Prop ≝ λty,v.
+  match ty with
+  [ ASTint sz sg ⇒
+    match v with
+    [ Vint sz' sg' ⇒ sz = sz' (* The sign does not matter *)
+    | _ ⇒ False ]
+  | ASTptr ⇒
+    match v with
+    [ Vptr p ⇒ True
+    | _ ⇒ False ]
+  | ASTfloat fsz ⇒
+    match v with
+    [ Vfloat _ ⇒ True
+    | _ ⇒ False ]   
+  ].
+
+
+definition type_consistent_with_value : type → val → Prop ≝ λty,v.
+match access_mode ty with
+[ By_value chunk ⇒ ast_typ_consistent_with_value chunk v
+| _ ⇒ True
+].
+
+
+(* We also need the following property. It is not provable unless [v] and [ty] are consistent. *)
+lemma fe_to_be_values_size :
+  ∀ty,v. ast_typ_consistent_with_value ty v →
+         typesize ty = |fe_to_be_values ty v|.
+*
+[ 1: #sz #sg #v
+     whd in match (fe_to_be_values ??); cases v
+     normalize in ⊢ (% → ?);
+     [ 1,4: @False_ind
+     | 2: #sz' #i normalize in ⊢ (% → ?); #Heq destruct normalize nodelta
+          >map_bounded >bytes_of_bitvector_bounded cases sz' //
+     | 3: #f normalize in ⊢ (% → ?); @False_ind
+     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
+| 2: #v cases v
+     normalize in ⊢ (% → ?);
+     [ 1,4: @False_ind
+     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
+     | 3: #f normalize in ⊢ (% → ?); @False_ind
+     | 5: #p #_ // ]
+| 3: #fsz #v cases v
+     normalize in ⊢ (% → ?); 
+     [ 1: @False_ind
+     | 2: #sz' #i normalize in ⊢ (% → ?); @False_ind
+     | 3: #f #_ cases fsz //
+     | 4: @False_ind
+     | 5: #p normalize in ⊢ (% → ?); @False_ind ]
+] qed.
+
+(* Not verified for floats atm. Restricting to integers. *)
+lemma fe_to_be_to_fe_value : ∀sz,sg,v. 
+  ast_typ_consistent_with_value (ASTint sz sg) v →
+  (be_to_fe_value (ASTint sz sg) (fe_to_be_values (ASTint sz sg) v) = v).
+#sz #sg #v
+whd in match (fe_to_be_values ??);
+cases v normalize in ⊢ (% → ?);
+[ 1,4: @False_ind
+| 3: #f @False_ind
+| 5: #p @False_ind
+| 2: #sz' #i' #Heq normalize in Heq; destruct (Heq) normalize nodelta
+     cases sz' in i'; #i normalize nodelta
+     normalize in i;
+     whd in match (be_to_fe_value ??);
+     normalize in match (size_intsize ?);
+     whd in match (bytes_of_bitvector ??);
+     [ 1: lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i
+          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
+          whd in match (build_integer_val ??);
+          >(BitVector_O … ri) //
+     | 2: lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i
+          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
+          whd in match (build_integer_val ??);
+          normalize in match (size_intsize ?);
+          whd in match (bytes_of_bitvector ??);
+          lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri
+          <(vsplit_prod … Heq_ri) normalize nodelta >Heq_ri
+          whd in match (build_integer_val ??);
+          >(BitVector_O … rri) //
+     | 3: lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i
+          <(vsplit_prod … Heq_i) normalize nodelta >Heq_i
+          whd in match (build_integer_val ??);
+          normalize in match (size_intsize ?);
+          whd in match (bytes_of_bitvector ??);
+          lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB
+          <(vsplit_prod … Heq_iB) normalize nodelta >Heq_iB
+          whd in match (bytes_of_bitvector ??);
+          lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD
+          <(vsplit_prod … Heq_iD) normalize nodelta >Heq_iD
+          whd in match (bytes_of_bitvector ??);
+          lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF
+          <(vsplit_prod … Heq_iF) normalize nodelta >Heq_iF
+          >(BitVector_O … iH) @refl ]
+] qed.                   
+
+(* It turns out that the following property is not true in general. Floats are converted to
+   BVundef, which are converted back to Vundef. But we care only about ints.  *)
+lemma storev_loadv_ok :
+  ∀sz,sg,m,b,ofs,v,m'.
+    ast_typ_consistent_with_value (ASTint sz sg) v →
+    store (ASTint sz sg) m (mk_pointer b ofs) v = Some ? m' →
+    load (ASTint sz sg) m' (mk_pointer b ofs) = Some ? v.
+#sz #sg #m #b #ofs #v #m' #H
+whd in ⊢ ((??%?) → (??%?)); #Hstoren
+lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint sz sg) v) m m' b ofs Hstoren)
+>(fe_to_be_values_size … H) #H >H normalize nodelta
+>fe_to_be_to_fe_value try //
+qed.
+
+(* For the arguments exposed before, we restrict the lemma to ints.
+ *)
+lemma store_value_load_value_ok :
+  ∀sz,sg,m,b,ofs,v,m'.
+    type_consistent_with_value (Tint sz sg) v →
+    store_value_of_type (Tint sz sg) m b ofs v = Some ? m' →
+    load_value_of_type (Tint sz sg) m' b ofs = Some ? v.
+#sz #sg #m #b #ofs #v #m' #H lapply H whd in ⊢ (% → ?);
+cases v in H; normalize nodelta
+[ 1: #_ @False_ind | 2: #vsz #vi #H | 3: #vf #_ @False_ind | 4: #_ @False_ind | 5: #vp #_ @False_ind ]
+#Heq >Heq in H; #H
+(* The lack of control on unfolds is extremely annoying. *)
+whd in match (store_value_of_type ?????); #Hstoren
+lapply (storen_loadn_ok … (fe_to_be_values_bounded (ASTint vsz sg) (Vint vsz vi)) m m' b ofs Hstoren)
+whd in match (load_value_of_type ????);
+>(fe_to_be_values_size … H) #H' >H' normalize nodelta
+>fe_to_be_to_fe_value try //
+qed.
+
+lemma load_int_value_inversion : 
+  ∀t,m,p,sz,i. load_value_of_type' t m p = Some ? (Vint sz i) → ∃sg. t = Tint sz sg.
+#t #m * #b #o #sz #i whd in match (load_value_of_type' ???);
+cases t
+[ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
+whd in match (load_value_of_type ????);
+[ 4,5,6,7,9: #Habsurd destruct ]
+whd in match (be_to_fe_value ??);
+cases (loadn ???) normalize nodelta
+[ 1,3,5,7: #Habsurd destruct ]
+*
+[ 1,3,5,7: #Heq normalize in Heq; destruct ]
+#hd #tl
+[ 2,3,4: cases hd
+  [ 1,2,7,8,13,14: whd in match (be_to_fe_value ??); #Heq destruct
+  | 4,5,10,11,16,17: #HA #Heq destruct (Heq) cases (eqb ??∧?) in e0;
+      normalize nodelta #Heq' destruct
+  | 6,12,18: #ptr #part #Heq destruct cases (pointer_of_bevals ?) in e0;
+             #foo normalize #Habsurd destruct
+  | *: #op1 #op2 #part #Heq destruct ]
+| 1: #H destruct cases hd in e0; normalize nodelta
+  [ 1,2: #Heq destruct
+  | 3: #op1 #op2 #part #Habsurd destruct
+  | 4: #by whd in match (build_integer_val ??);
+       cases (build_integer ??) normalize nodelta
+       [ 1: #Heq destruct
+       | 2: #bv #Heq destruct /2 by ex_intro/ ]
+  | 5: #p cases (eqb ?? ∧ ?) normalize nodelta #Heq destruct
+  | 6: #ptr #part cases (pointer_of_bevals ?) #foo normalize nodelta #Heq destruct ]
+] qed.
+
+lemma opt_to_res_load_int_value_inversion :
+ ∀t,m,p,sz,i.
+ (opt_to_res val (msg FailedLoad) (load_value_of_type' t m p) = OK ? (Vint sz i))
+  → ∃sg. t = Tint sz sg.
+#t #m #p #sz #i whd in match (opt_to_res ???);
+lapply (load_int_value_inversion t m p sz i)
+cases (load_value_of_type' t m p)
+[ 1: #H normalize nodelta #Habsurd destruct
+| 2: #v #H normalize nodelta #Heq destruct lapply (H (refl ??)) *
+     #sg #Heq >Heq /2 by ex_intro/
+] qed.
+
+lemma res_inversion : ∀A,B:Type[0]. ∀e:res A. ∀f:A → res B. ∀res:B.
+  match e with
+  [ OK x ⇒ f x
+  | Error msg ⇒ Error ? msg ] = OK ? res →  
+  ∃res_e. e = OK ? res_e ∧ OK ? res = f res_e.
+#A #B * 
+[ 2: #err #f #res normalize nodelta #Habsurd destruct
+| 1: #a #f #res normalize nodelta #Heq destruct %{a} @conj try @refl >Heq @refl
+] qed.
+
+(* In order to prove the consistency of types wrt values, we need the following lemma. *)
+(*
+lemma exec_expr_Vint_type_inversion :
+  ∀ge,env,m,e,sz,i,tr. (exec_expr ge env m e=return 〈Vint sz i,tr〉) →
+                       ∃sg. typeof e = Tint sz sg.
+#ge #env #m * #ed #ty 
+@(expr_ind2 … (λed,ty.∀sz:intsize.∀i:bvint sz.∀tr:trace.
+                  exec_expr ge env m (Expr ed ty)=return 〈Vint sz i,tr〉 →
+                  ∃sg:signedness.typeof (Expr ed ty)=Tint sz sg) … (Expr ed ty))
+[ 1: #e' #ty' #H @H
+| 2: #sz #i #t #sz0 #i0 #tr whd in ⊢ ((??%?) → ?); cases t
+     [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
+     [ 1: @(eq_intsize_elim … sz tsz) normalize nodelta
+          [ 2: #Hsz_eq destruct (Hsz_eq) normalize #Heq destruct (Heq)
+               %{tsg} @refl
+          | 1: #_ normalize #Habsurd destruct (Habsurd) ]
+     | *: #Habsurd normalize in Habsurd; destruct ]
+| 3: #f #t #sz #i #tr whd in ⊢ ((??%?) → ?); #H normalize in H; destruct (H)
+| 4: #id #t #sz #i #tr whd in ⊢ ((??%?) → ?);
+      @(match exec_lvalue' ge env m (Evar id) t
+        return λr. r = exec_lvalue' ge env m (Evar id) t → ?
+        with
+        [ OK x ⇒ λHeq. ?
+        | Error msg ⇒ λHeq. ?
+        ] (refl ? (exec_lvalue' ge env m (Evar id) t))) normalize nodelta
+     [ 2: normalize #Habsurd destruct ] #Hload
+     cases (bind_inversion ????? Hload) #loadval * #Heq_loadval #Heq_res
+     normalize in Heq_res; destruct (Heq_res)
+     -Hload
+     whd in Heq_loadval:(??%%); lapply Heq_loadval
+      @(match load_value_of_type' t m (\fst  x)
+        return λr. r = load_value_of_type' t m (\fst  x) → ?
+        with
+        [ None ⇒ λHeq. ?
+        | Some v' ⇒ λHeq. ?
+        ] (refl ? (load_value_of_type' t m (\fst  x)))) normalize nodelta
+     [ 1: #Habsurd destruct ]
+     #Heq_v' destruct (Heq_v')
+     cases (load_int_value_inversion … (sym_eq ??? Heq)) #sg #Htyp_eq
+     >Htyp_eq %{sg} @refl
+| 5: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?);
+     whd in match (exec_lvalue' ?????);
+     @(match exec_expr ge env m e
+       return λx. x = (exec_expr ge env m e) → ?
+       with
+       [ OK res ⇒ λH. ?
+       | Error msg ⇒ λH. ? ] (refl ? (exec_expr ge env m e)))
+      normalize nodelta
+     [ 2: #Habsurd destruct ]
+     cases res in H; #vres #trres #Hexec #H     
+     cases (res_inversion ????? H) -H * * #b' #o' #tr' *
+     cases vres in Hexec; normalize nodelta
+     [ 1: #_ #Habsurd destruct
+     | 2: #sz' #i' #_ #Habsurd destruct
+     | 3: #f #_ #Habsurd destruct
+     | 4: #_ #Habsurd destruct ]
+     #p #Heq_exec_expr #Heq destruct (Heq) #Heq
+     lapply (sym_eq ??? Heq) -Heq #Heq
+     cases (bind_inversion ????? Heq) -Heq #x * #Hload_value
+     #Heq normalize in Heq; destruct (Heq)
+     @(opt_to_res_load_int_value_inversion … Hload_value)
+| 6: #e #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H
+     cases (res_inversion ????? H) * * #b #o #tr * #Hexec_lvalue
+     cases t
+     [ 2: #tsz #tsg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] normalize nodelta
+     #Habsurd destruct
+| 7: #op #arg #t #Hind #sz #i #tr whd in ⊢ ((??%%) → ?); #H
+      cases (res_inversion ????? H) * #v #tr * #Hexec_expr
+      #H' lapply (sym_eq ??? H') -H' #H'
+      cases (bind_inversion ????? H') #v' * #Hopt_sem #Hvalues
+      normalize in Hvalues:(??%%); destruct (Hvalues) -H' -H
+      
+      lapp
+      >Hopt_sem in H';
+      destruct (Hvalues)
+      
+     whd in match (exec_lvalue ????);*)
+     
+
+
 
 (* Main theorem. To be ported and completed to memory injections. TODO *)
 theorem switch_removal_correction :
-  ∀ge,ge',s1, s1', tr, s2.
+  ∀ge,ge'.
   switch_removal_globals ? fundef_switch_removal ge ge' →
+  ∀s1,s1',tr,s2.
   switch_state_sim ge s1 s1' →
-  exec_step ge s1 = Value … 〈tr,s2〉 →
-  eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
-#ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
-@cthulhu
-qed.
-
-(*
+  exec_step ge s1 = Value … 〈tr,s2〉 →  
+  ∃n. after_n_steps (S n) … clight_exec ge' s1'
+  (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
+#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
 inversion Hsim_state
 [ 1: (* regular state *)
-  #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
+  #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
   #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp
-  #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge
+  #sss_env_hyp #sss_writeable_hyp #sss_result_rec #sss_result_hyp #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge
+  #Hs1_eq #Hs1_eq'
   elim (sim_related_globals … ge ge'
              sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars
              sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
-  #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
+  #Hsim_expr #Hsim_lvalue #_
+  (* II. Case analysis on the statement. *)
   cases sss_statement in sss_lu_fresh sss_result_hyp;
   (* Perform the intros for the statements *)
@@ -3026 +3914 @@
   | 14: #lab | 15: #cost #body ]
   #sss_lu_fresh #sss_result_hyp
-  [ 1: (* Skip *)
-    whd in match (switch_removal ???) in sss_result_hyp;
-    <(some_inj ??? sss_result_hyp)
+  [ 1: (* Skip statement *)
+    whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj <sss_result_hyp
+    (* III. Case analysis on the continuation. *)
     inversion sss_k_hyp normalize nodelta
-    [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step
-         @(eventually_now ????) whd in match (exec_step ??);
+    [ 1: #new_vars #Hnew_vars_eq #Hk #Hk' #_ #Hexec_step %{0} whd whd in ⊢ (??%?);
          >(prod_eq_lproj ????? sss_func_hyp)
          >fn_return_simplify
          whd in match (exec_step ??) in Hexec_step;
+         (* IV. Case analysis on the return type *)
          cases (fn_return sss_func) in Hexec_step;
          [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
@@ -3040 +3928 @@
          normalize nodelta
          whd in ⊢ ((??%?) → ?);
-         [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))}
-              @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)}
-              [ 1: @(lset_difference ? sss_writeable (blocks_of_env sss_env_ext))
-              | 3: @swc_stop
-              | 2:
-*)
-    
+         [ 1: #H destruct (H) % try @refl
+              /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/
+         | *: #Habsurd destruct (Habsurd) ]
+    | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp
+         #Hexec_step %{0} whd
+         >(prod_eq_lproj ????? sss_func_hyp)
+         whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl
+         <sss_func_hyp 
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         %1{u (refl ? (switch_removal s u))} try assumption try @refl         
+         #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind
+    | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec_step %{0} whd whd in Hexec_step;
+         >(prod_eq_lproj ????? sss_func_hyp)
+         whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl         
+         %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl
+         [ 1: <sss_func_hyp @refl
+         | 2: destruct normalize cases (switch_removal ??) * #body' #fvs' #u' @refl
+         | 3: whd in match (switch_removal ??); 
+              cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H
+         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+    | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')    
+         #Hexec_step %{0} whd whd in Hexec_step:(??%?) ⊢ (??%?);
+         cases (bindIO_inversion ??????? Hexec_step) #x1 * #Hexec
+         >(Hsim_expr … Hexec)
+         >bindIO_Value cases (exec_bool_of_val ??)
+         [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+         #b whd in match (m_bind ?????); whd in match (m_bind ?????);
+         cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H)
+         try @conj try @refl
+         [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try //
+              [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl
+              | 2: whd in match (switch_removal ??); 
+                   cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H
+              | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+         | 2: %{u … (switch_removal Sskip u) } try assumption try //
+              [ 1: @(fresh_for_Sskip … Hfresh)
+              | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+    | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_
+         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step)
+         @conj try @refl
+         %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try //
+         #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+    | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
+         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
+         %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try //
+         [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * //
+         | 2: whd in match (switch_removal ??) in Hincl;
+              cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta
+              cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta
+              whd in match (ret_vars ??); /2 by All_append_l/
+         | 3: @(swc_for3 … u) //
+         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+    | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
+         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
+         %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)}
+         try //
+         [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize
+              cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize
+              cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl
+         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+    | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
+         %1{sss_lu … new_vars … sss_writeable} try // try assumption
+         [ 1: destruct (sss_result_hyp) @refl
+         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+    | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_
+         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
+         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
+         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?);
+         >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify
+         cases (fn_return sss_func) in Hexec; normalize nodelta
+         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
+         #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
+         /3 by sws_returnstate, swc_call, memext_free_extended_environment/
+    ]
+  | 2: (* Assign statement *)
+       lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim
+       #Hexec %{0} whd in sss_result_hyp:(??%?);
+       cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs
+       cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs
+       cases (bindIO_inversion ??????? Hexec_rhs) #xs * #Heq_store #Hexec_store
+       whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta
+       >(Hsim … Heq_lhs) whd in match (m_bind ?????);
+       >(Hsim_expr … Heq_rhs) >bindIO_Value
+       lapply (memext_store_value_of_type' sss_m sss_m_ext xs sss_writeable (typeof lhs) (\fst  xl) (\fst  xr) sss_mem_hyp ?)
+       [ 1: cases (store_value_of_type' ????) in Heq_store;
+            [ 1: normalize #Habsurd destruct (Habsurd)
+            | 2: #m normalize #Heq destruct (Heq) @refl ] ]
+       * #m_ext' * #Hstore_eq #Hnew_ext >Hstore_eq whd in match (m_bind ?????);
+       whd destruct @conj try @refl
+       %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip  sss_lu) } try // try assumption
+       [ 1: @(fresh_for_Sskip … sss_lu_fresh)
+       | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+  | 3: (* Call statement *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp)
+       whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta
+       whd in Hexec:(??%?);
+       cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func
+       cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args
+       cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq
+       cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret
+       >(Hsim_expr … Heq_func) whd in match (m_bind ?????);
+       >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args)
+       whd in ⊢ (??%?);
+       >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))
+       whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert
+       whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret
+       @(option_ind … retv) normalize nodelta
+       [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl
+            %2{sss_writeable … sss_mem_hyp}
+            cases called_fundef
+            [ 2: #id #tl #ty @I
+            | 1: #called_function whd
+                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
+                 [ 1: <sss_func_hyp @refl ] #H >H -H
+                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
+                 [ 1: <sss_func_hyp @refl ] #H >H -H
+                 @(swc_call … sss_k_hyp) try assumption
+                 <sss_func_hyp @refl ]
+       | 2: #ret_expr #Hexec_ret_expr
+            cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret
+            whd in ⊢ ((??%%) → (??%%)); #H destruct (H)
+            >(exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret)
+            whd in ⊢ (??%?); whd @conj try @refl
+            cut (sss_func_tr = \fst (function_switch_removal sss_func))
+            [ 1: <sss_func_hyp @refl ] #H >H -H
+            @(sws_callstate … sss_writeable … sss_mem_hyp)
+            cases called_fundef
+            [ 2: #id #tl #ty @I
+            | 1: #called_function whd
+                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
+                 [ 1: <sss_func_hyp @refl ] #H >H -H
+                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
+                 [ 1: <sss_func_hyp @refl ] #H >H -H
+                 @(swc_call … sss_k_hyp) try assumption
+                 <sss_func_hyp @refl ] ]
+  | 4: (* Sequence statement *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)
+       >sss_result_proj <sss_result_hyp
+       cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
+       cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
+       normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try //
+       [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * //
+       | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
+            /2 by All_append_l/
+       | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+       @(swc_seq … u') try //
+       [ 2: >HeqB @refl
+       | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ
+            lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H
+       | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
+            /2 by All_append_r/
+       ]
+  | 5: (* If-then-else *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
+       cases (switch_removal_elim iftrue sss_lu) #iftrue' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
+       cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
+       whd whd in ⊢ (??%?);
+       cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
+       cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult
+       whd in Hresult:(??%%); destruct (Hresult)
+       >(Hsim_expr … Heq_cond) >bindIO_Value
+       >Heq_bool whd in match (m_bind ?????); whd @conj try @refl
+       cases b normalize nodelta
+       [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try //
+             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
+             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
+                  /2 by All_append_l/
+             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+       | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try //
+             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_
+                   @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H
+             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
+                  /2 by All_append_r/                   
+             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+  | 6: (* While loop *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
+       >sss_result_proj <sss_result_hyp whd
+       cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
+       cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool whd in ⊢ ((??%%) → ?);
+       cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
+       whd in ⊢ (? → (??%?));
+       >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool
+       whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult)
+       whd @conj try @refl
+       [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try //
+             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
+             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
+             | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+             | 3: @(swc_while … sss_lu) try // 
+                  [ 1: >HeqA @refl
+                  | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H ]
+             ]
+       | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try //
+            [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte;
+                 @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh)
+            | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+  | 7: (* do while loop *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
+       >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?);
+       cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
+       whd @conj try @refl
+       %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) } 
+       try assumption try //
+       [ 1:  lapply (fresh_to_substatements … sss_lu_fresh) normalize * //
+       | 2: >HeqA @refl
+       | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
+       | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+       | 4: @(swc_dowhile … sss_lu) try assumption try //
+            [ 1: >HeqA @refl
+            | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H            
+            ] ]        
+  | 8: (* for loop *)
+       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
+       >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?);
+       cases (switch_removal_elim init sss_lu) #init' * #fvs1' * #u' #HeqA >HeqA normalize nodelta
+       cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta
+       cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta
+       lapply Hexec
+       @(match is_Sskip init with
+       [ inl Heq ⇒ ?
+       | inr Hneq ⇒ ?
+       ]) normalize nodelta
+       [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf
+            whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta
+            #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl
+            %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try //
+            [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * //
+            | 2: >HeqA @refl
+            | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta
+                 >HeqB normalize nodelta >HeqC normalize nodelta
+                 /2 by All_append_l/
+            | 4: @(swc_for1 … u') try assumption try //
+                 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ
+                      @for_fresh_lift
+                      [ 1: @(fresher_for_univ … HY) 
+                      | 2: @(fresher_for_univ … HZ)
+                      | 3: @(fresher_for_univ … HX) ]
+                      lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs
+                 | 2: normalize >HeqB normalize nodelta >HeqC @refl
+                 | 3: lapply sss_incl <sss_result_hyp
+                      whd in match (ret_vars ??) in ⊢ (% → %); 
+                      whd in match (switch_removal ??) in ⊢ (% → %);
+                      >HeqA normalize nodelta >HeqB normalize nodelta >HeqC
+                      normalize nodelta #H /2 by All_append_r/
+                  ] ]
+       | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond
+            cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool
+            destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA')
+            normalize nodelta
+            >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec'
+            whd in match (m_bind ?????); >Heq_bool
+            cases b in Hexec'; normalize nodelta whd in match (bindIO ??????);
+            normalize #Hexec'' destruct (Hexec'') @conj try @refl
+            [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try //
+                 [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_
+                      @fresher_for_univ lapply (switch_removal_fte step u') >HeqB
+                      #H @H
+                 | 2: >HeqC @refl
+                 | 3: lapply sss_incl <sss_result_hyp
+                      whd in match (ret_vars ??) in ⊢ (% → %);
+                      whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta
+                      >HeqB normalize nodelta >HeqC normalize nodelta
+                      /2 by All_append_r/
+                 | 4: @(swc_for2 … u') try assumption
+                      [ 1: >HeqB @refl 
+                      | 2: >HeqB >HeqC @refl
+                      | 3: lapply sss_incl <sss_result_hyp
+                           whd in match (ret_vars ??) in ⊢ (% → %);
+                           whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta
+                           >HeqB normalize nodelta >HeqC normalize nodelta #H @H
+                      ]
+                 ]
+            | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try //
+                 [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ]
+        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+  | 9: (* break *)
+       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
+       lapply Hexec -Hexec
+       inversion sss_k_hyp
+       [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd)
+       | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq
+            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try //
+       | 3,4: #e #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
+       | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try //
+       | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' 
+            #Hres1 #Hres2 #Hincl #_ #Hnew_vars
+            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
+       | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk' #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 
+            #Heq destruct (Heq) whd @conj try @refl destruct
+            %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try //
+       | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold #Hdisjoint #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
+            #Heq destruct (Heq) ]
+       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+  | 10: (* continue *)
+       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
+       lapply Hexec -Hexec
+       inversion sss_k_hyp
+       [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd)
+       | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq
+            #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
+       | 3: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct
+            %1{uk … (switch_removal (Swhile ek sk) uk)} try assumption try //
+            [ 1: normalize cases (switch_removal sk uk) * #sk' #fvs' #uk' @refl
+            | 2: whd in match (switch_removal ??); lapply Hincl
+                 cases (switch_removal sk uk) * #body' #fvs' #uk'
+                 /2 by All_append_r/ ]                 
+       | 4: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
+            #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Hexec
+            cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond
+            cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hexec_bool
+            >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????);
+            cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?);
+            #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl
+            [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try //
+                 [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl
+                 | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk)
+                      * #body' #fvs' #uk' #H @H
+                 ]
+            | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try //
+                 try @(fresh_for_Sskip … Hfresh_suk) ]
+       | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
+       | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_
+            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl
+            destruct %1{uk … (switch_removal s1k uk)} try assumption try //
+            [ 1: cases (fresh_to_substatements … Hfresh_suk) * * //
+            | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?);
+                 whd in match (switch_removal ??);
+                 cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta
+                 cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta
+                 /2 by All_append_l/
+            | 3: @(swc_for3 … uk) try assumption try //
+            ]
+       | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_ 
+            whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq)
+            whd @conj try @refl destruct
+            %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try //
+       | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint
+             #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
+            #Heq destruct (Heq) ]
+       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+  | 11: (* return *)
+        #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
+        >sss_result_proj <sss_result_hyp normalize nodelta 
+        cases retval in sss_lu_fresh sss_result_hyp; normalize nodelta
+        [ 1: #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?));
+             >(prod_eq_lproj ????? sss_func_hyp)
+             >fn_return_simplify
+             cases (fn_return sss_func) normalize nodelta
+             [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
+             | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
+             [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl
+                  /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/
+             | *: #Habsurd destruct (Habsurd) ]
+        | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?));
+             >(prod_eq_lproj ????? sss_func_hyp)
+             >fn_return_simplify
+             @(match type_eq_dec (fn_return sss_func) Tvoid with
+               [ inl H ⇒ ?
+               | inr H ⇒ ? ]) normalize nodelta
+             [ 1: #Habsurd destruct (Habsurd)
+             | 2: #Hexec
+                   cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret
+                   whd in Hexec_ret:(??%%); destruct (Hexec_ret)
+                   >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd
+                   @conj try @refl
+                   /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/
+             ] ]
+  | 12: (* switch ! at long last *)
+        #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
+        >sss_result_proj <sss_result_hyp normalize nodelta #Hexec
+        cases (bindIO_inversion ??????? Hexec) * #condval #condtrace
+        cases condval normalize nodelta
+        [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 3: #f * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
+        #sz #i * #Hexec_eq #Heq whd in Heq:(??%%); destruct (Heq)
+
+        cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq
+        >Hbranch_eq normalize nodelta
+        cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta
+        cases (simplify_switch_elim (Expr (Evar new) (typeof cond)) switchcases' u'') #simplified * #u'''
+        #Hswitch_eq >Hswitch_eq normalize nodelta
+        %{1} whd whd in ⊢ (??%?); 
+        (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *)
+        whd in match (exec_lvalue ????);
+        (* show that the resulting ident is in the memory extension and that the lookup succeeds *)
+        -Hexec >Hbranch_eq in sss_result_hyp; normalize nodelta
+        >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta #sss_result_hyp
+        <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl
+        cases sss_env_hyp *
+        #Hlookup_new_in_old
+        #Hlookup_new_in_new
+        #Hlookup_old
+        lapply (Hlookup_new_in_new new ?)
+          [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem;
+             [ 1: @False_ind
+             | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% →  (??%?)); *
+                  [ 1: #Heq destruct (Heq)
+                       cases (identifier_eq_i_i … hdv) #Hrefl #Heq >Heq -Heq normalize nodelta
+                       @refl
+                  | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl
+                  cases (identifier_eq ? new hdv) normalize nodelta
+                  [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ]
+       * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????);
+       (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *)
+       >(Hsim_expr … Hexec_eq) >bindIO_Value
+       (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need
+             to set up things so that loading from that fresh location will yield exactly the stored value. *)
+       normalize in match store_value_of_type'; normalize nodelta
+       @cthulhu                
+   | *: @cthulhu ]
+ | *: @cthulhu ] qed.