Changeset 2227 for src/Clight/switchRemoval.ma

Timestamp:

Jul 20, 2012, 8:28:57 PM (9 years ago)

Author:

garnier

Message:

• New version of the switch removal algorithm, described at the top of the file.
• Memory injections (in a slightly weaker form than in Compcert, sufficient for this file) and related lemmas
• Ongoing: proof of semantics preservation for expression evaluation under memory injections. Progressively

port old proofs to the new setting.

File:

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

src/Clight/switchRemoval.ma

@@ -1 @@
-include "Clight/Csyntax.ma".
+ include "Clight/Csyntax.ma".
 include "Clight/fresh.ma".
 include "basics/lists/list.ma".
@@ -5 +5 @@
 include "Clight/Cexec.ma".
 include "Clight/CexecInd.ma".
+include "Clight/frontend_misc.ma".
+(*
+include "Clight/maps_obsequiv.ma".
+*)
+
 
 (* -----------------------------------------------------------------------------
@@ -61 +66 @@
 (* -----------------------------------------------------------------------------
    Definitions allowing to state that the program resulting of the transformation
-   is switch-free. The actual proof is done using Russell.
-   ----------------------------------------------------------------------------*)
+   is switch-free.
+   ---------------------------------------------------------------------------- *)
 
 (* Property of a Clight statement of containing no switch. Could be generalized into a kind of
@@ -85 +90 @@
 ].
 
-definition sf_statement ≝ Σs:statement. switch_free s.
-
-definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).
-
 (* Property of a list of labeled statements of being switch-free *)
 let rec branches_switch_free (sts : labeled_statements) : Prop ≝ 
 match sts with
-[ LSdefault st => 
+[ LSdefault st =>
   switch_free st
 | LScase _ _ st tl => 
@@ -98 +99 @@
 ].
 
-let rec branch_switch_free_ind
+let rec branches_ind
   (sts : labeled_statements)
   (H   : labeled_statements → Prop)  
@@ -107 +108 @@
   defcase st
 | LScase sz int st tl ⇒
-  indcase sz int st tl (branch_switch_free_ind tl H defcase indcase)
+  indcase sz int st tl (branches_ind tl H defcase indcase)
 ].
-
 
 (* -----------------------------------------------------------------------------
    Switch-removal code for statements, functions and fundefs.
    ----------------------------------------------------------------------------*)
-
-(* Given a list of switch cases, prefixes each case by a fresh goto label. It is
-   assumed as an hypothesis that each sub-statement is already switch-free
-   (argument [H]). The whole function returns a list of labelled switch-free switch
-   cases, along the particular label of the default statement and its associated
-   statement. A fresh label generator [uv] is threaded through the function.  *)
-let rec add_starting_lbl_list
-  (l : labeled_statements)  
-  (H : branches_switch_free l)
-  (uv : universe SymbolTag)
-  (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝
-match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with
-[ LSdefault st ⇒ λEq.
-  let 〈default_lab, uv'〉 ≝ fresh ? uv in
-  〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉
-| LScase sz tag st other_cases ⇒ λEq.
-  let 〈lab, uv'〉 ≝ fresh ? uv in
-  let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in
-  add_starting_lbl_list other_cases ? uv' acc'
-] (refl ? l).
-[ 1: destruct whd in H; //
-| 2: letin H1 ≝ H >Eq in H1; 
-  #H' normalize in H'; elim H' //
-| 3: >Eq in H; normalize * //
-] qed.
 
 (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
@@ -170 +145 @@
 
 (* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
+(*
 let rec produce_cond 
   (e : expr) 
@@ -203 +179 @@
   [ 1: @convert_break_lift elim case_statement //
   | 2: elim sub_statement // ]
-] qed.
+] qed. *)
 
 (* We assume that the expression e is consistely typed w.r.t. the switch branches *)
+(*
 let rec produce_cond2
   (e : expr)
@@ -237 +214 @@
           | 2: // ]
      | 2: elim sub_statement // ]
-] qed.     
-
-(* takes an expression, a list of switch-free cases and a freshgen and returns a 
- * switch-free equivalent, along an updated freshgen and a new local variable
- * (for storing the value of the expr). *)
-definition simplify_switch : 
-  expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝
-λe.λswitch_cases.λH.λuv.
+] qed. *)
+
+(*  (def_case : ident × sf_statement) *)
+
+let rec produce_cond
+  (e : expr)
+  (switch_cases : labeled_statements)
+  (u : universe SymbolTag)
+  (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝
+match switch_cases with
+[ LSdefault st ⇒  
+  let 〈lab,u1〉 ≝ fresh ? u in
+  let st' ≝ convert_break_to_goto st exit in
+  〈Slabel lab st', lab, u1〉
+| LScase sz tag st other_cases ⇒
+  let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in
+  let st' ≝ convert_break_to_goto st exit in
+  let 〈lab, u2〉 ≝ fresh ? u1 in
+  let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in
+  let case_statement ≝
+       Sifthenelse test
+        (Slabel lab (Ssequence st' (Sgoto sub_label)))
+        Sskip
+  in
+  〈Ssequence case_statement sub_statements, lab, u2〉
+].
+
+definition simplify_switch ≝
+   λ(e : expr).
+   λ(switch_cases : labeled_statements).
+   λ(uv : universe SymbolTag).
  let 〈exit_label, uv1〉            ≝ fresh ? uv in
- let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in
- let 〈result, useless_label〉      ≝ produce_cond2 e switch_cases defcase exit_label in
- 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉.
-[ 1:  normalize try @conj try @conj try // elim result //
-| 2: @H ]
-qed.
-
-(* recursively convert a statement into a switch-free one. *)
-let rec switch_removal 
-  (st : statement)
-  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
-match st return λs.s = st → ? with
-[ Sskip       ⇒ λEq. 〈«st,?», [ ], uv〉
-| Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
-| Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
-| Ssequence s1 s2 ⇒ λEq. 
-  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
-  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
-  〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
-| Sifthenelse e s1 s2 ⇒ λEq. 
-  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
-  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
-  〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
-| Swhile e body ⇒ λEq.
-  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
-  〈«Swhile e (pi1 … body'),?», vars', uv'〉 
-| Sdowhile e body ⇒ λEq.
-  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
-  〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 
-| Sfor s1 e s2 s3 ⇒ λEq.
-  let 〈s1', vars1, uv'〉   ≝ switch_removal s1 uv in
-  let 〈s2', vars2, uv''〉  ≝ switch_removal s2 uv' in
-  let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in
-  〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉
-| Sbreak ⇒ λEq.
-  〈«st,?», [ ], uv〉
-| Scontinue ⇒ λEq.
-  〈«st,?», [ ], uv〉
-| Sreturn _ ⇒ λEq.
-  〈«st,?», [ ], uv〉
-| Sswitch e branches ⇒ λEq.
-   let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in
-   match sf_branches with
-   [ mk_Sig branches' H ⇒ 
-     let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in
-     let ident             ≝ Expr (Evar switch_tmp) (typeof e) in
-     let assign            ≝ Sassign ident e in     
-     let 〈result, uv3〉     ≝ simplify_switch ident branches' H uv2 in
-     〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉
+ let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in
+ 〈Ssequence result (Slabel exit_label Sskip), uv2〉.
+
+lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))).
+#l @(labeled_statements_ind … l) 
+[ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 
+     normalize in Hsf ⊢ %; @(convert_break_lift … Hsf)
+| 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl
+     #e #lab #u normalize
+     lapply (Hind Hsf_tl e lab u)
+     cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta
+     cases (fresh ??) #lab0 #u2 normalize nodelta
+     normalize try @conj try @conj try @conj try //
+     @(convert_break_lift … Hsf_hd)
+] qed.
+
+lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)).
+#e #l cases l
+[ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta
+     whd @conj whd
+     [ 1: @convert_break_lift assumption
+     | 2: @I ]
+| 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u
+     cases (fresh ? u) #exit_label #uv1 normalize nodelta
+     lapply (produce_cond_switch_free tl Hsftl e exit_label uv1)
+     cases (produce_cond e tl uv1 exit_label)
+     * #cond #lab #u1 #Hsf_cond normalize nodelta
+     cases (fresh ??) #lab0 #u2 normalize nodelta
+     normalize @conj try @conj try @conj try @conj try //
+     @(convert_break_lift ?? Hsf)
+] 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})  }.
+      
+(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
+   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
+   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
+   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
+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) ≝
+match st with
+[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
+| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
+| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, 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''〉
+| 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''〉
+| Swhile e body ⇒
+  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
+  ret 〈Swhile e body', acc, fvs', u'〉
+| Sdowhile e body ⇒
+  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
+  ret 〈Sdowhile e body', acc, fvs', 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'''〉
+| Sbreak ⇒
+  ret 〈st, [ ], fvs, u〉
+| Scontinue ⇒
+  ret 〈st, [ ], fvs, u〉
+| Sreturn _ ⇒
+  ret 〈st, [ ], fvs, 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'〉
    ]
-| Slabel label body ⇒ λEq.
-  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
-  〈«Slabel label (pi1 … body'), ?», vars', uv'〉
-| Sgoto _ ⇒ λEq.
-  〈«st, ?», [ ], uv〉
-| Scost cost body ⇒ λEq.
-  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
-  〈«Scost cost (pi1 … body'),?», vars', uv'〉 
-] (refl ? st)
+| Slabel label body ⇒
+  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
+  ret 〈Slabel label body', acc, fvs', u'〉
+| Sgoto _ ⇒
+  ret 〈st, [ ], fvs, u〉
+| Scost cost body ⇒
+  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
+  ret 〈Scost cost body', acc, fvs', u'〉 
+]
 
 and switch_removal_branches 
   (l : labeled_statements) 
-  (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
+  (fvs : list ident) 
+  (u : universe SymbolTag)
+(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
 match l with
 [ LSdefault st ⇒
-  let 〈st, vars',  uv'〉 ≝ switch_removal st uv in
-  〈«LSdefault (pi1 … st), ?», vars', uv'〉
+  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
+  ret 〈LSdefault st', acc1, fvs', u'〉
 | LScase sz int st tl =>
-  let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in
-  let 〈st', vars'', uv''〉     ≝ switch_removal st uv' in 
-  〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉
+  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''〉
 ].
-try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try //
-[ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj //
-| 2: elim result //
-| 3: elim st //
-| 4: elim st' //
-| 5: elim tl_result //
+
+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 function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝ 
-λf,u.
-  let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in
-  let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in
-  〈f, u'〉.
-
-let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝
-match f with
-[ CL_Internal f ⇒
-  let 〈f',u'〉 ≝ function_switch_removal f u in
-  〈CL_Internal f', u'〉
-| CL_External _ _ _ ⇒
-  〈f, 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 // ]
+     ] ]
+| *: 
+  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
+  @cthulhu ]
+qed.
 
 (* -----------------------------------------------------------------------------
@@ -356 +653 @@
  *)
 
+(* Least element in the total order of identifiers. *)
+definition least_identifier ≝ an_identifier SymbolTag one. 
+
 (* This is certainly overkill: variables adressed in an expression should be declared in the
- * enclosing function's prototype. *)
-let rec max_of_expr (e : expr) (current : ident) : ident ≝
+ * enclosing function's prototype. *) 
+let rec max_of_expr (e : expr) : ident ≝
 match e with
 [ Expr ed _ ⇒
   match ed with
-  [ Econst_int _ _ ⇒ current
-  | Econst_float _ ⇒ current
-  | Evar id ⇒ max_id id current
-  | Ederef e1 ⇒ max_of_expr e1 current
-  | Eaddrof e1 ⇒ max_of_expr e1 current
-  | Eunop _ e1 ⇒ max_of_expr e1 current
-  | Ebinop _ e1 e2 ⇒ max_of_expr e1 (max_of_expr e2 current)
-  | Ecast _ e1 ⇒ max_of_expr e1 current
-  | Econdition e1 e2 e3 ⇒
-    max_of_expr e1 (max_of_expr e2 (max_of_expr e3 current))
+  [ Econst_int _ _ ⇒ least_identifier
+  | Econst_float _ ⇒ least_identifier
+  | Evar id ⇒ id
+  | Ederef e1 ⇒ max_of_expr e1
+  | Eaddrof e1 ⇒ max_of_expr e1
+  | Eunop _ e1 ⇒ max_of_expr e1
+  | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
+  | Ecast _ e1 ⇒ max_of_expr e1
+  | Econdition e1 e2 e3 ⇒  
+    max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3))
   | Eandbool e1 e2 ⇒
-    max_of_expr e1 (max_of_expr e2 current)
+    max_id (max_of_expr e1) (max_of_expr e2)
   | Eorbool e1 e2 ⇒
-    max_of_expr e1 (max_of_expr e2 current)
-  | Esizeof _ ⇒ current
-  | Efield r f ⇒ max_id f (max_of_expr r current)
-  | Ecost _ e1 ⇒ max_of_expr e1 current
+    max_id (max_of_expr e1) (max_of_expr e2)  
+  | Esizeof _ ⇒ least_identifier
+  | Efield r f ⇒ max_id f (max_of_expr r)
+  | Ecost _ e1 ⇒ max_of_expr e1
   ]
 ].
 
-(* Reeasoning about this promises to be a serious pain. Especially the Scall case. *)
-let rec max_of_statement (s : statement) (current : ident) : ident ≝
+(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
+let rec max_of_statement (s : statement) : ident ≝
 match s with
-[ Sskip ⇒ current
-| Sassign e1 e2 ⇒ max_of_expr e2 (max_of_expr e1 current)
-| Scall ret f args ⇒
+[ Sskip ⇒ least_identifier
+| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
+| Scall r f args ⇒
   let retmax ≝ 
-    match ret with
-    [ None ⇒ current
-    | Some e ⇒ max_of_expr e current ]
+    match r with
+    [ None ⇒ least_identifier
+    | Some e ⇒ max_of_expr e ]
   in
-  foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args
-| Ssequence s1 s2 ⇒ 
-  max_of_statement s1 (max_of_statement s2 current)
+  max_id (max_of_expr f) 
+         (max_id retmax
+                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
+| Ssequence s1 s2 ⇒
+  max_id (max_of_statement s1) (max_of_statement s2)
 | Sifthenelse e s1 s2 ⇒
-  max_of_expr e (max_of_statement s1 (max_of_statement s2 current))
+  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
 | Swhile e body ⇒
-  max_of_expr e (max_of_statement body current)
+  max_id (max_of_expr e) (max_of_statement body)
 | Sdowhile e body ⇒
-  max_of_expr e (max_of_statement body current)
+  max_id (max_of_expr e) (max_of_statement body)
 | Sfor init test incr body ⇒
-  max_of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current)))
-| Sbreak ⇒ current
-| Scontinue ⇒ current
+  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
+| Sbreak ⇒ least_identifier
+| Scontinue ⇒ least_identifier
 | Sreturn opt ⇒
   match opt with
-  [ None ⇒ current
-  | Some e ⇒ max_of_expr e current
+  [ None ⇒ least_identifier
+  | Some e ⇒ max_of_expr e
   ]
 | Sswitch e ls ⇒
-  max_of_expr e (max_of_ls ls current)
+  max_id (max_of_expr e) (max_of_ls ls)
 | Slabel lab body ⇒
-  max_id lab (max_of_statement body current)
+  max_id lab (max_of_statement body)
 | Sgoto lab ⇒
-  max_id lab current
+  lab
 | Scost _ body ⇒
-  max_of_statement body current  
+  max_of_statement body
 ]
-and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝
+and max_of_ls (ls : labeled_statements) : ident ≝
 match ls with
-[ LSdefault s ⇒ max_of_statement s current
-| LScase _ _ s ls' ⇒ max_of_ls ls' (max_of_statement s current)
+[ LSdefault s ⇒ max_of_statement s
+| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
 ].
 
 definition max_id_of_function : function → ident ≝
-λf. max_of_statement (fn_body f) (max_id_of_fn f).
-
-definition max_id_of_fundef_deep : clight_fundef → ident ≝
-λf. match f with
-  [ CL_Internal f ⇒ max_id_of_function f
-  | CL_External id _ _ ⇒ id
-  ].
-
-let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝
-let func_max ≝
-  foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs
-in max_id func_max current.
-
-definition max_id_of_program_deep : clight_program → ident ≝
-λp.
-  max_id
-    (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p))
-    (max_id_of_globvars (prog_vars ?? p)).
-        
-(* The previous functions compute an (over?)-approximation of the identifiers and labels.
-   The following function builds a "good" universe for a complete clight program. *)
-definition universe_for_program_deep : clight_program → universe SymbolTag ≝
-λp. universe_of_max (max_id_of_program_deep p).
-
+λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f).
+
+(* We compute fresh universes on a function-by function basis, since there can't
+ * be cross-functions gotos or stuff like that. *)
+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 rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
+match f with
+[ CL_Internal f ⇒
+  CL_Internal (\fst (function_switch_removal f))
+| CL_External _ _ _ ⇒
+  f
+].
 
 let rec program_switch_removal (p : clight_program) : clight_program ≝
- let uv         ≝ universe_for_program_deep p in
  let prog_funcs ≝ prog_funct ?? p in
- let 〈sf_funcs, final_uv〉 ≝ 
-  foldr ?? (λcl_fundef.λacc.
-    let 〈fundefs, uv1〉    ≝ acc in    
-    let 〈fun_id, fun_def〉 ≝ cl_fundef in
-    let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in
-    〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉
-   ) 〈[ ], uv〉 prog_funcs 
- in 
+ let sf_funcs   ≝ map ?? (λcl_fundef. 
+    let 〈fun_id, fun_def〉 ≝ cl_fundef in 
+    〈fun_id, fundef_switch_removal fun_def〉
+  ) prog_funcs in
  mk_program ??
   (prog_vars … p)
@@ -468 +768 @@
   (prog_main … p).
 
+
+(* -----------------------------------------------------------------------------
+   Applying two relations on all substatements and all subexprs (directly under). 
+   ---------------------------------------------------------------------------- *)
+
+let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝
+match s1 with
+[ Sskip ⇒ True
+| Sassign e1 e2 ⇒ Q e1 ∧ Q e2
+| Scall r f args ⇒
+  match r with
+  [ None ⇒ Q f ∧ (All … Q args)
+  | Some r ⇒ Q r ∧ Q f ∧ (All … Q args)
+  ]
+| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
+| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
+| Swhile e sub ⇒ Q e ∧ P sub
+| Sdowhile e sub ⇒ Q e ∧ P sub
+| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
+| Sbreak ⇒ True
+| Scontinue ⇒ True
+| Sreturn r ⇒
+  match r with
+  [ None ⇒ True
+  | Some r ⇒ Q r ]
+| Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P)
+| Slabel _ sub ⇒ P sub
+| Sgoto _ ⇒ True
+| Scost _ sub ⇒ P sub
+]
+and substatement_ls ls (P : statement → Prop) : Prop ≝
+match ls with
+[ LSdefault sub ⇒ P sub
+| LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P)
+].
+
+(* -----------------------------------------------------------------------------
+   Freshness conservation results on switch removal.
+   ---------------------------------------------------------------------------- *)
+
+(* Similar stuff in toCminor.ma. *)
+lemma fresh_for_univ_still_fresh :
+   ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'.
+* #p * #i #H1 #v * #p' lapply H1 normalize
+#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.
+
+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 → 
+ 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.
+
+(*
+lemma switch_removal_fresh : ∀i,s,u. 
+    fresh_for_univ ? i u → 
+    fresh_for_univ ? i (\snd (switch_removal s u)).
+#i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u →
+                                      fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s)
+try //
+[ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp
+     whd in match (switch_removal (Ssequence s1' s2') u);
+     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta
+     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
+     * #irr3 #irr4 #uB #HuB normalize nodelta //
+| 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp
+     whd in match (switch_removal (Sifthenelse e s1' s2') u);
+     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta
+     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
+     * #irr3 #irr4 #uB #HuB normalize nodelta //
+| 3,4: #e #s' #Hind #u #Hyp
+     whd in match (switch_removal ? u);
+     lapply (Hind u Hyp) elim (switch_removal s' u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta //
+| 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp
+     whd in match (switch_removal (Sfor s1' e s2' s3') u);
+     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta
+     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
+     * #irr3 #irr4 #uB #HuB normalize nodelta
+     lapply (Hind3 uB HuB) elim (switch_removal s3' uB)
+     * #irr5 #irr6 #uC #HuC normalize nodelta //
+| 6: #e #ls #Hind #u #Hyp
+     whd in match (switch_removal (Sswitch e ls) u);
+     lapply (Hind u Hyp)
+     cases (switch_removal_branches ls u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta
+     lapply (fresh_for_univ_still_fresh … HuA)
+     cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉))
+     -Haux #HuA' normalize nodelta
+     lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA')
+     cases (simplify_switch ???) #stm #uB
+     #Haux normalize nodelta //
+| 7,8: #label #body #Hind #u #Hyp
+     whd in match (switch_removal ? u);
+     lapply (Hind u Hyp) elim (switch_removal body u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta //
+| 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??);
+     lapply (Hind u Hyp) elim (switch_removal defcase u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta //
+| 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize
+     lapply (Hind2 u Hyp) elim (switch_removal_branches tl u)
+     * #irr1 #irr2 #uA #HuA normalize nodelta
+     lapply (Hind1 uA HuA) elim (switch_removal s0 uA)
+     * #irr3 #irr4 #uB #HuB //
+] qed.
+
+lemma switch_removal_branches_fresh : ∀i,ls,u. 
+    fresh_for_univ ? i u → 
+    fresh_for_univ ? i (\snd (switch_removal_branches ls u)).
+#i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u →
+                                           fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls)
+try /2 by switch_removal_fresh/
+[ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh)
+     cases (switch_removal s u) * //
+| 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize
+     lapply (Htl u Hfresh)
+     cases (switch_removal_branches tl u) * normalize nodelta
+     #ls' #fvs #u' #Hfresh'
+     lapply (Hs u' Hfresh')
+     cases (switch_removal s u') * //
+] qed.
+*)
 (* -----------------------------------------------------------------------------
    Simulation proof and related voodoo.
    ----------------------------------------------------------------------------*)
-
-(* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *)
-inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
-| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
-| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
 
 definition expr_lvalue_ind_combined ≝
@@ -539 +982 @@
 ].
 
+
 (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
    by a non-constant number of evaluations in the converted program. More precisely, 
@@ -544 +988 @@
    necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
    
-(* A version of simplify_switch hiding the ugly proj *)
-definition sw_rem : statement → (universe SymbolTag) → statement ≝
-λs,u.
-  \fst (\fst (switch_removal s u)).
-
+(* A version of simplify_switch hiding the ugly projs *)
 definition fresh_for_expression ≝
-λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u.  
-  
+λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.
+
 definition fresh_for_statement ≝
-λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u.
-
+λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.
+
+(* needed during mutual induction ... *)
+definition fresh_for_labeled_statements ≝ 
+λls,u. fresh_for_univ ? (max_of_ls ls) u.
+   
 definition fresh_for_function ≝
 λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.
 
-let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝
-match k with
-[ Kstop ⇒ True
-| Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u)
-| Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
-| Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
-| Kfor2 e s1 s2 k0 ⇒
-  (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
-  (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
-| Kfor3 e s1 s2 k0 ⇒
-  (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
-  (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
-| Kswitch k0 ⇒ fresh_for_continuation k0 u
-| Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u)
-].
-
-inductive switch_cont_sim : cont → cont → Prop ≝
-| swc_stop : 
-    switch_cont_sim Kstop Kstop
-| swc_seq : ∀s,k,k',u.
-    fresh_for_statement s u →
-    switch_cont_sim k k' → 
-    switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k')
-| swc_while : ∀e,s,k,k',u.
-    fresh_for_expression e u →
-    fresh_for_statement s u →
-    switch_cont_sim k k' →
-    switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k')
-| swc_dowhile : ∀e,s,k,k',u.
-    fresh_for_expression e u →
-    fresh_for_statement s u →
-    switch_cont_sim k k' →
-    switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k')
-| swc_for1 : ∀e,s1,s2,k,k',u1,u2.
-    fresh_for_statement s1 u1 →
-    fresh_for_statement s2 u2 →
-    switch_cont_sim k k' →
-    switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k')
-| swc_for2 : ∀e,s1,s2,k,k',u1,u2.
-    fresh_for_statement s1 u1 →
-    fresh_for_statement s2 u2 →
-    switch_cont_sim k k' →
-    switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k')
-| swc_for3 : ∀e,s1,s2,k,k',u1,u2.
-    fresh_for_statement s1 u1 →
-    fresh_for_statement s2 u2 →
-    switch_cont_sim k k' → 
-    switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k')
-| swc_switch : ∀k,k'.
-    switch_cont_sim k k' → 
-    switch_cont_sim (Kswitch k) (Kswitch k')
-| swc_call : ∀r,f,en,k,k',u. 
-    fresh_for_function f u →
-    switch_cont_sim k k' →
-    switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k').
-
-
-inductive switch_state_sim : state → state → Prop ≝
-| sws_state : ∀uf,us,uk,f,s,k,k',e,m.
-    fresh_for_function f uf →
-    fresh_for_statement s us →
-    fresh_for_continuation k' uk →
-    switch_cont_sim k k' → 
-    switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m)
-(* Extra matching states that we can reach that don't quite correspond to the
-   labelling function *)
-(*   
-| sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
-    switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
-| sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
-    switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
-| sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
-    switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
-*)
-(* and the rest *)
-| sws_callstate : ∀ufd,fd,args,k,k',m. 
-    switch_cont_sim k k' → 
-    switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m)
-| sws_returnstate : ∀res,k,k',m. 
-    switch_cont_sim k k' → 
-    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
-| sws_finalstate : ∀r. 
-    switch_state_sim (Finalstate r) (Finalstate r)
-.
-
-inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
-| eventually_base : ∀s,t,s'. 
-    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
-    P s' →
-    eventually ge P s t
-| eventually_step : ∀s,t,s',t'.
-    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
-    eventually ge P s' t' →
-    eventually ge P s (t ⧺ t').
-    
-(* [eventually] is not so nice to use directly, we would like to make the mandatory
- * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
-   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
-lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
-                                      eventually ge P s t.
-#ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP}
-qed.
-
-record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
-  rg_find_symbol: ∀s.
-    find_symbol ? ge s = find_symbol ? ge' s;
-  rg_find_funct: ∀v,f.
-    find_funct ? ge v = Some ? f →
-    find_funct ? ge' v = Some ? (t f);
-  rg_find_funct_ptr: ∀b,f.
-    find_funct_ptr ? ge b = Some ? f →
-    find_funct_ptr ? ge' b = Some ? (t f)
-}.
-
-(* TODO ... fundef_switch_removal wants a universe which is fresh-for-its argument. *)
-(*
-lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' → 
-  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
-  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
-*)  
-
-(* The return type of any function is invariant under switch removal *)
-lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f.
-#f #u elim f #ret #args #vars #body normalize elim (switch_removal body u)
-* * #body' #Hswitch_free #new_vars #u' normalize //
-qed.
-
-lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0).
-#e0 #s0 #us0 normalize 
-cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize //
-qed.
+(* misc properties of the max function on positives. *)
 
 lemma max_one_neutral : ∀v. max v one = v.
@@ -723 +1037 @@
 #a @(le_to_leb_true a a) // qed.
 
-(*
-lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False.
-#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq
-destruct inversion H2 
-[ 2: #m #H1 #H2 #H3
-elim b; normalize in match (succ ?);
-[ 1: #H destruct (H)
-| 2: #p #H 
-*)
 (* This should be somewhere else. *)
 lemma associative_max : associative ? max.
@@ -777 +1082 @@
           #Hca /2/
      ]
-] qed.       
+] qed.   
 
 lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
 * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
 qed.
-
+(*
 lemma max_of_expr_rewrite : 
   ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
@@ -812 +1117 @@
       whd in match (max_id ??); >associative_max @refl
 ] qed.
-
+*)
+lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u.
+* #a * #b * #u normalize
+lapply (pos_compare_to_Prop a b)
+cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
+[ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/
+| 2: destruct >reflexive_leb /2/
+| 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/
+] 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 = 
+  max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l).
+#l elim l
+[ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl
+| 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%);
+     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
+] qed.
+
+(* -----------------------------------------------------------------------------
+   Stuff on memory and environments extensions.
+   Let us recap: the memory model of a function is in two layers. An environment
+   (type [env]) maps identifiers to blocks, and a memory maps blocks
+   switch_removal introduces new, fresh variables. What is to be noted is that
+   switch_removal modifies both the contents of the "disjoint" part of memory, but
+   also where the data is allocated. The first solution considered was to consider
+   an extensional equivalence relation on values, saying that equivalent pointers
+   point to equivalent values. This has to be a coinductive relation, in order to
+   take into account cyclic data structures. Rather than using coinductive types,
+   we use the compcert solution, using so-called memory embeddings. 
+   ---------------------------------------------------------------------------- *)
+
+(* ---------------- *)
+(* auxillary lemmas *)
+lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
+#a #b #HA
+lapply (Zltb_true_to_Zlt … HA) #HA_prop
+@Zlt_to_Zltb_true /2/
+qed.
+
+lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
+#a @Zlt_to_Zltb_true /2/ qed.
+
+
+definition le_offset : offset → offset → bool ≝
+  λx,y. Zleb (offv x) (offv y).
+  
+lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
+
+lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
+
+(* When equality on A is decidable, [mem A elt l] is too. *)
+lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
+#A #dec #elt #l elim l
+[ 1: normalize %2 /2/
+| 2: #hd #tl #Hind
+     elim (dec elt hd)
+     [ 1: #Heq >Heq %1 /2/
+     | 2: #Hneq cases Hind
+        [ 1: #Hmem %1 /2/
+        | 2: #Hnmem %2 normalize
+              % #H cases H
+              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
+              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
+] ] ]
+qed.
+
+lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
+#a #b @(eq_block_elim … a b) /2/ qed.
+
+lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
+#l #elt1 #elt2 elim l
+[ 1: normalize #Habsurd @(False_ind … Habsurd)
+| 2: #hd #tl #Hind normalize #Hl #Hr
+   cases Hl
+   [ 1: #Heq >Heq
+        @(eq_block_elim … hd elt2)
+        [ 1: #Heq >Heq /2 by not_to_not/
+        | 2: #x @x ]
+   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
+        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
+        | 2: #Hmem2 @Hind //
+        ]
+   ]
+] qed.
+
+lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
+#b1 #b2 * #Hb
+@(eq_block_elim … b1 b2)
+[ 1: #Habsurd @(False_ind … (Hb Habsurd))
+| 2: // ] qed.
+
+(* Type of blocks in a particular region. *)
+definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg.
+
+(* An embedding is a function from blocks to (blocks+offset). *)
+definition embedding ≝ block → option (block × offset).
+
+definition offset_plus : offset → offset → offset ≝
+  λo1,o2. mk_offset (offv o1 + offv o2).
+  
+lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o.
+* #z normalize // qed.
+
+(* Translates a pointer through an embedding. *)
+definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
+λp,E.
+match p with
+[ mk_pointer pblock poff ⇒
+   match E pblock with
+   [ None ⇒ None ?
+   | Some loc ⇒
+    let 〈dest_block,dest_off〉 ≝ loc in
+    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
+    Some ? ptr
+   ]
+].
+
+(* We parameterise the "equivalence" relation on values with an embedding. *)
+(* Front-end values. *)
+inductive value_eq (E : embedding) : val → val → Prop ≝
+| undef_eq : ∀v.
+  value_eq E Vundef v
+| vint_eq : ∀sz,i. 
+  value_eq E (Vint sz i) (Vint sz i)
+| vfloat_eq : ∀f.
+  value_eq E (Vfloat f) (Vfloat f)
+| vnull_eq :
+  value_eq E Vnull Vnull
+| vptr_eq : ∀p1,p2.
+  pointer_translation p1 E = Some ? p2 →
+  value_eq E (Vptr p1) (Vptr p2).
+  
+(* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
+ * the values are equivalent. *)
+definition load_sim ≝
+λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
+ ∀b1,off1,b2,off2,ty,v1.
+  valid_block m1 b1 →
+  E b1 = Some ? 〈b2,off2〉 →
+  load_value_of_type ty m1 b1 off1 = Some ? v1 →
+  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
+
+(* Definition of a memory injection *)
+record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
+{ (* Load simulation *)
+  mi_inj : load_sim E m1 m2;
+  (* Invalid blocks are not mapped *)
+  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
+  (* Blocks in the codomain are valid *)
+  mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
+  (* Regions are preserved *)
+  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
+  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
+   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
+   * all variables are allocated in the same block. *)
+  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'. 
+                b1 ≠ b2 →
+                E b1 = Some ? 〈b1',o1'〉 →
+                E b2 = Some ? 〈b2',o2'〉 →
+                b1' ≠ b2'
+}.
+
+(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\ 
+ * A memory extension is a [memory_inj] with some particular blocks designated *)
+
+alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
+
+record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
+{ me_inj : memory_inj E m1 m2;
+  me_writeable : list block;
+  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
+  me_writeable_ok : ∀b,b',o'. 
+                    valid_block m1 b → 
+                    E b = Some ? 〈b',o'〉 →
+                    ¬ (meml ? b' me_writeable)
+}.
+
+(* ---------------------------------------------------------------------------- *)
+(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
+
+(* A particular inversion. *)
+lemma value_eq_ptr_inversion : 
+  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
+#E #p1 #v #Heq inversion Heq
+[ 1: #v #Habsurd destruct (Habsurd)
+| 2: #sz #i #Habsurd destruct (Habsurd)
+| 3: #f #Habsurd destruct (Habsurd)
+| 4:  #Habsurd destruct (Habsurd)
+| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct 
+     %{p2} @conj try @refl try assumption
+] qed.
+ 
+(* If we succeed to load something by value from a 〈b,off〉 location, 
+   [b] is a valid block. *)
+lemma load_by_value_success_valid_block_aux :
+  ∀ty,m,b,off,v.
+    access_mode ty = By_value (typ_of_type ty) →
+    load_value_of_type ty m b off = Some ? v →
+    Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)
+#ty #m * #brg #bid #off #v whd in match (valid_block ??);
+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 match (load_value_of_type ????);
+[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
+#Hmode
+[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
+     normalize in match (typesize ?); 
+     whd in match (loadn ???);
+     whd in match (beloadv ??);
+     cases (Zltb bid (nextblock m)) normalize nodelta
+     try // #Habsurd destruct (Habsurd)
+| *: normalize in Hmode; destruct (Hmode)
+] qed.
+
+
+lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
+* #rg #id #m normalize
+elim id /2/ qed.
+
+lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
+* #rg #id #m normalize
+elim id /2/ qed.
+
+lemma load_by_value_success_valid_block :
+  ∀ty,m,b,off,v.
+    access_mode ty = By_value (typ_of_type ty) → 
+    load_value_of_type ty m b off = Some ? v → 
+    valid_block m b.
+#ty #m #b #off #v #Haccess_mode #Hload
+@valid_block_from_bool
+@(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload)
+qed.
+
+(* Making explicit the contents of memory_inj for load_value_of_type *)
+lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
+    memory_inj E m1 m2 →
+    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
+    load_value_of_type ty m1 b1 off1 = Some ? v1 →
+    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
+#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
+lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
+     normalize in Hembed;
+     lapply (mi_inj … Hinj b1 off1)
+     cases (E b1) in Hembed;
+     [ 1: normalize #Habsurd destruct (Habsurd)
+     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
+     lapply (refl ? (access_mode 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 ]
+     normalize in ⊢ ((???%) → ?); #Hmode #Hyp
+     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
+     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
+     #Hload_success
+     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
+     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
+qed.
+
+
+(* -------------------------------------- *)
+(* Lemmas pertaining to memory allocation *)
+
+(* A valid block stays valid after an alloc. *)
+lemma alloc_valid_block_conservation :
+  ∀m,m',z1,z2,r,new_block.
+  alloc m z1 z2 r = 〈m', new_block〉 →
+  ∀b. valid_block m b → valid_block m' b.
+#m #m' #z1 #z2 #r * #b' #Hregion_eq
+elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
+#Halloc destruct (Halloc)
+#b whd in match (valid_block ??) in ⊢ (% → %); /2/
+qed.
+
+(* Allocating a new zone produces a valid block. *)
+lemma alloc_valid_new_block :
+  ∀m,m',z1,z2,r,new_block.
+  alloc m z1 z2 r = 〈m', new_block〉 →
+  valid_block m' new_block.
+* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
+whd in match (alloc ????); whd in match (valid_block ??);
+#Halloc destruct (Halloc) /2/
+qed.
+
+(* All data in a valid block is unchanged after an alloc. *)
+lemma alloc_beloadv_conservation :
+  ∀m,m',block,offset,z1,z2,r,new_block.
+    valid_block m block →
+    alloc m z1 z2 r = 〈m', new_block〉 →
+    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
+* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
+whd in Halloc:(??%?); destruct (Halloc)
+whd in match (beloadv ??) in ⊢ (??%%);
+lapply (valid_block_to_bool … Hvalid) #Hlt
+>Hlt >(zlt_succ … Hlt)
+normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
+cut (eqZb (block_id block) next = false)
+[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
+>Hneq cases (eq_region ??) normalize nodelta  @refl
+qed.
+
+(* Lift [alloc_beloadv_conservation] to loadn *)
+lemma alloc_loadn_conservation :
+  ∀m,m',z1,z2,r,new_block.
+    alloc m z1 z2 r = 〈m', new_block〉 →
+    ∀n. ∀block,offset.
+    valid_block m block →
+    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
+#m #m' #z1 #z2 #r #new_block #Halloc #n
+elim n try //
+#n' #Hind #block #offset #Hvalid_block
+whd in ⊢ (??%%);
+>(alloc_beloadv_conservation … Hvalid_block Halloc)
+cases (beloadv m' (mk_pointer block offset)) //
+#bev normalize nodelta
+whd in match (shift_pointer ???); >Hind try //
+qed.
+
+(* Memory allocation preserves [memory_inj] *)
+lemma alloc_memory_inj :
+  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
+  alloc m2 z1 z2 r = 〈m2', new_block〉 →
+  memory_inj E m1 m2'.
+#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
+%
+[ 1:
+  whd
+  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
+  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
+  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
+  lapply (refl ? (access_mode ty))
+  cases ty in Hload_eq;
+  [ 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 ]
+  #Hload normalize in ⊢ ((???%) → ?); #Haccess
+  [ 1,7,8: normalize in Hload; destruct (Hload)
+  | 2,3,4,9: whd in match (load_value_of_type ????);
+     whd in match (load_value_of_type ????);
+     lapply (load_by_value_success_valid_block … Haccess Hload)
+     #Hvalid_block
+     whd in match (load_value_of_type ????) in Hload;
+     <(alloc_loadn_conservation … Halloc … Hvalid_block) 
+     @Hload
+  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
+| 2: @(mi_freeblock … Hmemory_inj)
+| 3: #b #b' #o' #HE
+     lapply (mi_incl … Hmemory_inj … HE)
+     elim m2 in Halloc; #contents #nextblock #Hnextblock
+     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
+     whd in match (valid_block ??) in ⊢ (% → %); /2/
+| 4: @(mi_region … Hmemory_inj)
+| 5: @(mi_disjoint … Hmemory_inj)
+] qed.
+
+(* Memory allocation induces a memory extension. *)
+lemma alloc_memory_ext :
+  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
+  alloc m2 z1 z2 r = 〈m2', new_block〉 →
+  memory_ext E m1 m2'.
+#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
+lapply (alloc_memory_inj … Hmemory_inj Halloc)
+#Hinj' %
+[ 1: @Hinj'
+| 2: @[new_block]
+| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
+      #Heq destruct (Heq) whd elim m2 in Halloc;
+      #Hcontents #nextblock #Hnextblock
+      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
+      /2/
+| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
+     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
+     #Heq destruct (Heq) 
+     lapply (mi_incl … Hmemory_inj … Hload)
+     whd in ⊢ (% → ?); #Habsurd
+     (* contradiction car ¬ (valid_block m2 new_block)  *)
+     elim m2 in Halloc Habsurd;
+     #contents_m2 #nextblock_m2 #Hnextblock_m2
+     whd in ⊢ ((??%?) → ?);
+     #Heq_alloc destruct (Heq_alloc)
+     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
+] qed.
+
+lemma bestorev_beloadv_conservation :
+  ∀mA,mB,wb,wo,v. 
+    bestorev mA (mk_pointer wb wo) v = Some ? mB →
+    ∀rb,ro. eq_block wb rb = false →
+    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
+#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
+whd in ⊢ (??%%);
+elim mB in Hstore; #contentsB #nextblockB #HnextblockB
+normalize in ⊢ (% → ?);
+cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
+[ 2: #Habsurd destruct (Habsurd) ]
+cases (if Zleb (low (blocks mA wb)) (offv wo) 
+       then Zltb (offv wo) (high (blocks mA wb)) 
+       else false) normalize nodelta
+[ 2: #Habsurd destruct (Habsurd) ]
+#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
+cases rr cases wr normalize try //
+@(eqZb_elim … rid wid)
+[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
+try //
+qed.
+
+(* lift [bestorev_beloadv_conservation to [loadn] *)
+lemma bestorev_loadn_conservation :
+  ∀mA,mB,n,wb,wo,v. 
+    bestorev mA (mk_pointer wb wo) v = Some ? mB →
+    ∀rb,ro. eq_block wb rb = false →
+    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
+#mA #mB #n
+elim n
+[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
+| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
+     whd in ⊢ (??%%);
+     >(bestorev_beloadv_conservation … Hstore … Hneq)
+     >(Hind … Hstore … Hneq) @refl
+] qed.
+
+(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
+lemma bestorev_load_value_of_type_conservation :
+  ∀mA,mB,wb,wo,v. 
+    bestorev mA (mk_pointer wb wo) v = Some ? mB →
+    ∀rb,ro. eq_block wb rb = false →
+    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
+#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #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 ] try //
+[ 1: elim sz | 2: elim fsz | 3: | 4: ]
+whd in ⊢ (??%%);
+>(bestorev_loadn_conservation … Hstore … Hneq) @refl
+qed.
+
+(* Writing in the "extended" part of a memory preserves the underlying injection *)
+lemma bestorev_memory_ext_to_load_sim :
+  ∀E,mA,mB,mC.
+  ∀Hext:memory_ext E mA mB.
+  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
+  bestorev mB (mk_pointer wb wo) v = Some ? mC →
+  load_sim E mA mC.
+#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
+#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
+(* Show that (wb ≠ b2) *)
+lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
+lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
+cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
+<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
+@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
+qed.
+
+(* Writing in the "extended" part of a memory preserves the whole memory injection *)
+lemma bestorev_memory_ext_to_memory_inj :
+  ∀E,mA,mB,mC.
+  ∀Hext:memory_ext E mA mB.
+  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
+  bestorev mB (mk_pointer wb wo) v = Some ? mC →
+  memory_inj E mA mC.
+#E #mA * #contentsB #nextblockB #HnextblockB #mC
+#Hext #wb #wo #v #Hwb #Hstore
+%
+[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
+elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
+#Hmem
+[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
+whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
+normalize in ⊢ (% → ?); #Hlt_wb
+>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
+cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
+normalize nodelta
+[ 2: #Habsurd destruct (Habsurd) ]
+#Heq destruct (Heq)
+#b #b' #o' #Hembed @(Hcodomain … Hembed)
+qed.
+
+(* It even preserves memory extensions, with the same writeable blocks.  *)
+lemma bestorev_memory_ext_to_memory_ext :
+  ∀E,mA,mB.
+  ∀Hext:memory_ext E mA mB.
+  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
+  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
+  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
+#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
+%{(mk_memory_ext … 
+      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
+      (me_writeable … Hext)
+      ?
+      (me_writeable_ok … Hext)
+ )} try @refl
+#b #Hmemb
+lapply (me_writeable_valid … Hext b Hmemb)
+lapply (me_writeable_valid … Hext wb Hmem)
+elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
+lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
+>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
+cases (if Zleb (low (contentsB wb)) (offv wo) 
+       then Zltb (offv wo) (high (contentsB wb)) 
+       else false)
+normalize [ 2: #Habsurd destruct (Habsurd) ]
+#Heq destruct (Heq) @Hb_valid
+qed.
+
+(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
+lemma storen_memory_ext_to_memory_ext :
+  ∀E,mA,l,mB,mC.
+  ∀Hext:memory_ext E mA mB.
+  ∀wb,wo. meml ? wb (me_writeable … Hext) → 
+  storen mB (mk_pointer wb wo) l = Some ? mC →
+  memory_ext E mA mC.
+#E #mA #l elim l
+[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
+     @Hext 
+| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
+     whd in ⊢ ((??%?) → ?);
+     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
+     cases (bestorev mB (mk_pointer wb wo) hd)
+     normalize nodelta
+     [ 1: #H #Habsurd destruct (Habsurd) ]
+     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
+     @(Hind … HextD … Hstore)
+     <Heq @Hmem
+] qed.     
+
+(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
+lemma store_value_of_type_memory_ext_to_memory_ext :
+  ∀E,mA,mB,mC.
+  ∀Hext:memory_ext E mA mB.
+  ∀wb,wo. meml ? wb (me_writeable … Hext) → 
+  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
+  memory_ext E mA mC.
+#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
+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 (Habsurd) ]
+#Hstore
+@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
+qed.
+
+(* End of the memory injection-related stuff. *)
+(* ------------------------------------------ *)
+
+(* Lookup functions in list environments (used to type local variables in functions) *)      
+let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
+match l with
+[ nil ⇒ false
+| cons hd tl ⇒
+  let 〈id, ty〉 ≝ hd in
+  match identifier_eq SymbolTag i id with
+  [ inl Hid_eq ⇒ true
+  | inr Hid_neq ⇒ mem_assoc_env i tl  
+  ]
+].
+
+let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
+match l with
+[ nil ⇒ None ?
+| cons hd tl ⇒
+  let 〈id, ty〉 ≝ hd in
+  match identifier_eq SymbolTag i id with
+  [ inl Hid_eq ⇒ Some ? ty
+  | inr Hid_neq ⇒ assoc_env i tl  
+  ]
+].
+
+(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
+   of the environment [e1] s.t. the new binders are in [new], and such that those
+   new binders are "writeable" in the memory extension [Hext] *)
+definition disjoint_extension ≝
+λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
+λ(new : list (ident × type)). λ(E:embedding). λ(Hext: memory_ext E m1 m2).
+  ∀id. match mem_assoc_env id new with
+       [ true ⇒
+           ∃b. lookup ?? e2 id = Some ? b
+            ∧ meml ? b (me_writeable … Hext)
+            ∧ lookup ?? e1 id = None ?
+       | false ⇒
+         match lookup ?? e1 id with
+         [ None ⇒ lookup ?? e2 id = None ?
+         | Some b1 ⇒
+           match lookup ?? e2 id with
+           [ None ⇒ False
+           | Some b2 ⇒
+             valid_block m1 b1 ∧
+             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
+           ]
+         ]
+       ].
+
+(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
+ * the variable is not in a local environment, then we search into the global one.
+ * A proper "extension" of a local environment should be such that the extension
+ * does not collide with a given global env. 
+ * To see the details of why we need that, see [exec_lvalue'], Evar id case.
+ *)
+definition ext_fresh_for_genv ≝
+λ(ext : list (ident × type)). λ(ge : genv).
+  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.
+
+(* Any environment is a "disjoint" extension of itself with nothing. *)
+(*
+lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
+#e #m #ty #id
+normalize in match (mem_assoc_env id []); normalize nodelta
+cases (lookup ?? e id) try //
+#b normalize nodelta
+% #ty cases (load_value_of_type ????)
+[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
+cases (assoc_env id ty) //
+qed. *)
+
+
+(* "generic" simulation relation on [res ?] *)
+definition res_sim ≝
+  λ(A : Type[0]).
+  λ(eq : A → A → Prop).
+  λ(r1, r2 : res A).
+  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.
+
+(* Specialisation of [res_sim] to match [exec_expr] *)
+definition exec_expr_sim ≝ λE.
+  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).
+
+(* Specialisation of [res_sim] to match [exec_lvalue] *)
+definition exec_lvalue_sim ≝ λE.
+  res_sim (block × offset × trace)
+    (λr1,r2.
+      let 〈b1,o1,tr1〉 ≝ r1 in
+      let 〈b2,o2,tr2〉 ≝ r2 in
+      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).
+
+lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r.
+#ty #m #b #o cases (load_value_of_type ty m b o)
+[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.
+
+(*
+lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
+   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
+   〈f',vars〉 = function_switch_removal f →
+   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
+   environment_extension env env' vars. 
+
+#f #f'
+cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
+cases (fn_params f) cases (fn_vars f)
+[ 1: #vars >append_nil >append_nil >nil_append elim vars   
+   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
+   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
+        whd in ⊢ ((???(???%)) → ?);
+ #Henv #Hswrem #Henv'
+#id   
+*)
+
+(*
+lemma substatement_fresh : ∀s,u. 
+    fresh_for_statement s u →
+    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
+#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
+try /by I/
+[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
+| 2: *
+    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
+         #Hfresh_e #Hfresh_args @conj try assumption
+         normalize nodelta in Hfresh_args;
+         >max_id_commutative in Hfresh_args; >max_id_one_neutral
+         #Hfresh_args         
+    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
+         #Hfresh_e #H lapply (fresh_max_split ??? H) *
+         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
+    elim args in Hfresh_args;
+    [ 1,3: //
+    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
+            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
+            [ 1,3: @Hu 
+            | 2,4: @Hind assumption ] ] 
+| 3: #s1 #s2 #_ #_
+     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * 
+     whd in match (substatement_P ??); /2/
+| 4: #e #cond #iftrue #iffalse #_
+     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
+     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
+| 5,6: #e #stm #_
+     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
+| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
+      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
+      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
+| 8: #ret #H whd elim ret in H; try //      
+| 9: #expr #ls #Hind #H whd @conj
+     [ 1: elim (fresh_max_split … H) //
+     | 2: @Hind elim (fresh_max_split … H) // ]
+| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
+| 11: #sz #i #hd #tl #Hhd #Htl #H whd
+     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
+     @Htl //
+] qed.
+*)
+
+(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
+ * a local environment extended by some local variables. *)
+ 
+
+(* lookup on environment extension *)
+(*
+lemma extension_lookup :
+  ∀map, map', ext, id, result.
+  environment_extension map map' ext →
+  lookup ?? map id = Some ? result →
+  lookup ?? map' id = Some ? result.
+#map #map' #ext #id #result #Hext lapply (Hext id)
+cases (mem_assoc_env ??) normalize nodelta
+[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
+| 2: #H >H // ] qed.
+
+*)
+
+(* Extending a map by an empty list of variables yields an observationally equivalent
+ * environment. *)
+(* 
+lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
+* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
+[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
+     cases (lookup_opt block id map2) normalize
+     [ 1: >H #H2 >H2 @refl
+     | 2: #b >H cases v
+          [ 1: normalize * #H @(False_ind … H)
+          | 2: #block normalize // ] ]
+| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
+     >H cases v normalize try //
+     #block cases (lookup_opt ? id map1) normalize try //
+     * #H @(False_ind … H)
+] qed. *)
+
+(* If two identifier maps are observationally equal, then they contain the same bocks.
+ * see maps_obsequiv.ma for the details of the proof. *)
+(* 
+lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
+* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
+>Hfold @refl
+qed.
+*)
+
+(* 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.
+    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.
+    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.
+    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.
+    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.
+    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.
+    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)))
+      (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.
+*)
+
+inductive switch_state_sim : state → state → Prop ≝
+| sws_state : ∀u,f,s,k,k',m,m',result.
+    ∀env, env', f', vars.
+    ∀E:embedding.    
+    ∀Hext:memory_ext E m m'.
+    fresh_for_statement s u →
+    (*
+    env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
+    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
+    *)
+    〈f',vars〉 = function_switch_removal f →
+    disjoint_extension env m env' m' vars E Hext →
+    switch_removal s (map ?? (fst ??) vars) u = Some ? result → 
+    switch_cont_sim (map ?? (fst ??) vars) k k' →
+    switch_state_sim
+      (State f s k env m)
+      (State f' (ret_st ? result) k' env' m')
+| sws_callstate : ∀vars, fd,args,k,k',m.
+    switch_cont_sim vars k k' →
+    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 
+| sws_returnstate : ∀vars,res,k,k',m.
+    switch_cont_sim vars k k' →
+    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
+| sws_finalstate : ∀r.
+    switch_state_sim (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/
+qed.
+
+(* [eventually ge P s tr] states that after a finite number of [exec_step], the 
+   property P on states will be verified. *)
+inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
+| eventually_base : ∀s,t,s'.
+    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
+    P s' →
+    eventually ge P s t
+| eventually_step : ∀s,t,s',t',trace.
+    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
+    eventually ge P s' t' →
+    trace = (t ⧺ t') →
+    eventually ge P s trace.
+
+(* [eventually] is not so nice to use directly, we would like to make the mandatory
+ * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
+   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
+lemma eventually_now : ∀ge,P,s,t. 
+  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
+   eventually ge P s t.
+#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
+qed.
+(*   
+lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
+                                      ∃t'.eventually ge P s (t ⧺ t').
+#ge #P #s #t * #s' * #Hexec #HP %{E0} normalize >(append_nil ? t) %1{????? Hexec HP}
+qed.
+*)
+lemma eventually_later : ∀ge,P,s,t. 
+   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → 
+    eventually ge P s t.
+#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
+try assumption
+qed.
+
+(* lift value_eq to option block *)
+definition option_block_eq ≝ λE,ob1,ob2.
+match ob1 with
+[ None ⇒
+  match ob2 with
+  [ None ⇒ True
+  | Some _ ⇒ False ]
+| Some b1 ⇒
+  match ob2 with
+  [ None ⇒ False
+  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
+].
+
+definition value_eq_opt ≝ λE,ov1,ov2.
+match ov1 with
+[ None ⇒
+  match ov2 with
+  [ None ⇒ True
+  | Some _ ⇒ False ]
+| Some v1 ⇒
+  match ov2 with
+  [ None ⇒ False
+  | Some v2 ⇒ 
+    value_eq E v1 v2 ]
+].
+
+record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
+  rg_find_symbol: ∀s.
+    option_block_eq E (find_symbol ? ge s) (find_symbol ? ge' s);
+  rg_find_funct: ∀v,f.
+    find_funct ? ge v = Some ? f →
+    find_funct ? ge' v = Some ? (t f);
+  rg_find_funct_ptr: ∀b,f.
+    find_funct_ptr ? ge b = Some ? f →
+    find_funct_ptr ? ge' b = Some ? (t f)
+}.
+
+lemma exec_lvalue_expr_elim :
+  ∀E,r1,r2,Pok,Qok.
+  ∀H:exec_lvalue_sim E r1 r2.
+  (∀bo1,bo2,tr.
+    let 〈b1,o1〉 ≝ bo1 in
+    let 〈b2,o2〉 ≝ bo2 in
+    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
+    match Pok 〈bo1,tr〉 with
+    [ Error err ⇒ True
+    | OK vt1 ⇒
+      let 〈val1,trace1〉 ≝ vt1 in
+      match Qok 〈bo2,tr〉 with
+      [ Error err ⇒ False
+      | OK vt2 ⇒
+        let 〈val2,trace2〉 ≝ vt2 in
+        trace1 = trace2 ∧ value_eq E val1 val2      
+      ]
+    ]) →
+  exec_expr_sim E
+    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
+    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
+#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
+elim r1
+[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
+| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
+     * #a2 * #Hr2 >Hr2 normalize nodelta
+     elim a1 * #b1 #o1 #tr1
+     elim a2 * #b2 #o2 #tr2 normalize nodelta
+     * #Hvalue_eq #Htrace_eq #H2
+     destruct (Htrace_eq)
+     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
+     cases (Pok 〈b1, o1, tr2〉)
+     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
+     | 1: * #v1 #tr1' normalize nodelta #H3 whd
+          * #v1' #tr1'' #Heq destruct (Heq)
+          cases (Qok 〈b2,o2,tr2〉) in H3;
+          [ 2: #error #Hfalse @(False_ind … Hfalse)
+          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
+               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
+] ] ] qed.
+
+lemma exec_expr_expr_elim :
+  ∀E,r1,r2,Pok,Qok.
+  ∀H:exec_expr_sim E r1 r2.
+  (∀v1,v2,trace.
+    value_eq E v1 v2 →
+    match Pok 〈v1,trace〉 with
+    [ Error err ⇒ True
+    | OK vt1 ⇒
+      let 〈val1,trace1〉 ≝ vt1 in
+      match Qok 〈v2,trace〉 with
+      [ Error err ⇒ False
+      | OK vt2 ⇒
+        let 〈val2,trace2〉 ≝ vt2 in
+        trace1 = trace2 ∧ value_eq E val1 val2      
+      ]
+    ]) →
+  exec_expr_sim E
+    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
+    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
+#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
+elim r1
+[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
+| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
+     * #a2 * #Hr2 >Hr2 normalize nodelta
+     elim a1 #v1 #tr1
+     elim a2 #v2 #tr2 normalize nodelta
+     * #Hvalue_eq #Htrace_eq #H2
+     destruct (Htrace_eq)
+     lapply (H2 v1 v2 tr2 Hvalue_eq)
+     cases (Pok 〈v1, tr2〉)
+     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
+     | 1: * #v1 #tr1' normalize nodelta #H3 whd
+          * #v1' #tr1'' #Heq destruct (Heq)
+          cases (Qok 〈v2,tr2〉) in H3;
+          [ 2: #error #Hfalse @(False_ind … Hfalse)
+          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
+               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
+] ] ] qed.
+
+(* Commutation results of standard binary operations with value_eq. *)
+lemma unary_operation_value_eq :
+  ∀E,op,v1,v2,ty.
+   value_eq E v1 v2 →
+   ∀r1.
+   sem_unary_operation op v1 ty = Some ? r1 →
+    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
+#E #op #v1 #v2 #ty #Hvalue_eq #r1
+inversion Hvalue_eq
+[ 1: #v #Hv1 #Hv2 #_ destruct
+     cases op normalize
+     [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          normalize #Habsurd destruct (Habsurd)
+     | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          normalize #Habsurd destruct (Habsurd)
+     | 2: #Habsurd destruct (Habsurd) ]
+| 2: #vsz #i #Hv1 #Hv2 #_
+     cases op
+     [ 1: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
+          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
+               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
+               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
+               //
+          | *: #Habsurd destruct (Habsurd) ]
+     | 2: whd in match (sem_unary_operation ???);      
+          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
+     | 3: whd in match (sem_unary_operation ???);
+          cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          normalize nodelta
+          whd in ⊢ ((??%?) → ?);
+          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
+               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
+          | *: #Habsurd destruct (Habsurd) ] ]
+| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
+     cases op normalize nodelta
+     [ 1: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_notbool ??);
+          #Heq1 destruct
+          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
+     | 2: normalize #Habsurd destruct (Habsurd)
+     | 3: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_neg ??);
+          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
+| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
+     cases op normalize nodelta
+     [ 1: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_notbool ??);
+          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
+     | 2: normalize #Habsurd destruct (Habsurd)
+     | 3: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_neg ??);
+          #Heq1 destruct ]
+| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
+     cases op normalize nodelta
+     [ 1: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_notbool ??);          
+          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
+     | 2: normalize #Habsurd destruct (Habsurd)
+     | 3: cases ty
+          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+          whd in match (sem_neg ??);          
+          #Heq1 destruct ]
+]
+qed.
+
+(* A cleaner version of inversion for [value_eq] *)
+lemma value_eq_inversion :
+  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → 
+  (∀v. P Vundef v) →
+  (∀sz,i. P (Vint sz i) (Vint sz i)) →
+  (∀f. P (Vfloat f) (Vfloat f)) →
+  (P Vnull Vnull) →
+  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
+  P v1 v2.
+#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
+inversion Heq
+[ 1: #v #Hv1 #Hv2 #_ destruct @H1
+| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
+| 3: #f #Hv1 #Hv2 #_ destruct @H3
+| 4: #Hv1 #Hv2 #_ destruct @H4
+| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
+
+(* value_eq lifts to addition *)
+lemma add_value_eq :
+  ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2.
+   value_eq E v1 v2 →
+   value_eq E v1' v2' →
+   memory_inj E m1 m2 → (* This injection seems useless TODO *)
+   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
+           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
+#E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
+@(value_eq_inversion E … Hvalue_eq1)
+[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
+[ 1: whd in match (sem_add ????); normalize nodelta
+     cases (classify_add ty1 ty2) normalize nodelta
+     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
+     #Habsurd destruct (Habsurd)
+| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
+     cases (classify_add ty1 ty2) normalize nodelta     
+     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
+     [ 2,3,5: #Habsurd destruct (Habsurd) ]
+     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
+     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
+     [ 1: @intsize_eq_elim_elim
+          [ 1: #_ #Habsurd destruct (Habsurd)
+          | 2: #Heq destruct (Heq) normalize nodelta
+               #Heq destruct (Heq)
+               /3 by ex_intro, conj, vint_eq/ ]
+     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
+          /3 by ex_intro, conj, vint_eq/
+     | 3: #Heq destruct (Heq)
+          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
+          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
+          @vptr_eq whd in match (pointer_translation ??);
+          cases (E b1') in Hembed;
+          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
+          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
+               whd in match (shift_pointer_n ????);
+               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
+                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
+               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
+               #Heq >Heq @refl ]
+     ]
+| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
+     cases (classify_add ty1 ty2) normalize nodelta     
+     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
+     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
+     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
+     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
+     #Heq destruct (Heq)
+     /3 by ex_intro, conj, vfloat_eq/
+| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
+     cases (classify_add ty1 ty2) normalize nodelta     
+     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
+     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
+     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
+     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
+     @eq_bv_elim 
+     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
+     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
+| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
+     cases (classify_add ty1 ty2) normalize nodelta
+     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
+     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
+     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
+     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
+     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
+     #Heq destruct (Heq)
+     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
+     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
+     elim p1 in Hembed; #b1 #o1 normalize nodelta
+     cases (E b1)
+     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
+     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
+          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
+          @refl
+     ]
+] qed.
+          
+(* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *)
+
+
+(* Commutation result for binary operators. *)
+lemma binary_operation_value_eq :
+  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
+   value_eq E v1 v2 →
+   value_eq E v1' v2' →
+   memory_inj E m1 m2 →
+   ∀r1.
+   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
+   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
+#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
+cases op
+whd in match (sem_binary_operation ??????);
+whd in match (sem_binary_operation ??????);
+@cthulhu
+qed.
+
+ 
+(* Simulation relation on expressions *)
+lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
+  ∀E:embedding.
+  ∀Hext:memory_ext E m1 m2.
+  switch_removal_globals E ? fundef_switch_removal ge ge' →
+  disjoint_extension en1 m1 en2 m2 ext E Hext →
+  ext_fresh_for_genv ext ge →
+  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
+  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
+#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
+@expr_lvalue_ind_combined
+[ 1: #csz #cty #i #a1
+     whd in match (exec_expr ????); elim cty
+     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+     normalize nodelta
+     [ 2: cases (eq_intsize csz sz) normalize nodelta
+          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
+          | 2: #Habsurd destruct (Habsurd) ]
+     | 4,5,6: #_ #H destruct (H)
+     | *: #H destruct (H) ]
+| 2: #ty #fl #a1
+     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
+| 3: *
+  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
+  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
+  #ty whd in ⊢ (% → ?); #Hind try @I
+  whd in match (Plvalue ???);
+  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
+       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
+       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
+       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
+           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
+           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
+           whd in match (load_value_of_type' ???); 
+           whd in match (load_value_of_type' ???);
+           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
+           cases (load_value_of_type ty m1 bl1 o1)
+           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
+                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
+                    normalize /4 by ex_intro, conj/
+  ] ] ]
+| 4: #v #ty whd * * #b1 #o1 #tr1
+     whd in match (exec_lvalue' ?????);
+     whd in match (exec_lvalue' ?????);
+     lapply (Hdisjoint v)
+     lapply (Hext_fresh_for_genv v)
+     cases (mem_assoc_env v ext) #Hglobal
+     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
+          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
+          >(Hglobal (refl ??)) normalize
+          #Habsurd destruct (Habsurd)
+     | 2: normalize nodelta
+          cases (lookup ?? en1 v) normalize nodelta
+          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
+               lapply (rg_find_symbol … Hrelated v)
+               cases (find_symbol ???) normalize
+               [ 1: #_ #Habsurd destruct (Habsurd)
+               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
+                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
+                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
+                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
+                         normalize /2/
+                ] ]
+         | 2: #block
+              cases (lookup ?? en2 v) normalize nodelta
+              [ 1: #Hfalse @(False_ind … Hfalse)
+              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
+                   %{〈b, zero_offset, E0〉} @conj try @refl
+                   normalize /2/
+    ] ] ]
+| 5: #e #ty whd in ⊢ (% → %);
+     whd in match (exec_lvalue' ?????);
+     whd in match (exec_lvalue' ?????);
+     cases (exec_expr ge en1 m1 e)
+     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
+          * elim v1 normalize nodelta
+          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
+          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
+          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
+          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
+          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
+               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
+               #Hvalue_eq normalize
+               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
+               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
+               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
+               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
+               normalize @conj // ]
+     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
+| 6: #ty #e #ty'
+     #Hsim @(exec_lvalue_expr_elim … Hsim)
+     cases ty
+     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
+     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
+     #tr #H @conj try @refl try assumption
+| 7: #ty #op #e
+     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
+     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
+     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
+     [ 1: #_ @I
+     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
+           normalize /2/ ]
+| *: @cthulhu ] qed.
+
+(* TODO: Old cases, to be ported to memory injection.
+| 8: #ty #op #e1 #e2 #Hind1 #Hind2
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     @(exec_expr_expr_elim … Hind1)
+     cases (exec_expr ge en1 m1 e2) in Hind2;
+     [ 2: #error normalize //
+     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
+          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
+          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
+
+
+| 9: #ty #castty #e #Hind
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     cases Hind
+     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1: cases (exec_expr ge en m e)
+          [ 2: #error #_ @SimFail /2 by ex_intro/
+          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 
+          ] 
+     ]
+| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     cases Hind1
+     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1: cases (exec_expr ge en m e1)
+          [ 2: #error #_ @SimFail /2 by ex_intro/
+          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
+               normalize nodelta
+               cases (exec_bool_of_val ??)
+               [ 2: #error @SimFail /2 by ex_intro/
+               | 1: * whd in match (m_bind ?????); normalize nodelta
+                    [ 1: cases Hind2
+                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+                         | 1: cases (exec_expr ge en m e2)
+                              [ 2: #error #_  @SimFail /2 by ex_intro/
+                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
+                                   @SimOk normalize nodelta #a2
+                                   whd in match (m_bind ?????); // ]
+                         ]
+                    | 2: cases Hind3
+                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+                         | 1: cases (exec_expr ge en m e3)
+                              [ 2: #error #_  @SimFail /2 by ex_intro/
+                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
+                                   @SimOk normalize nodelta #a3
+                                   whd in match (m_bind ?????); // ]
+                         ]
+     ] ] ] ]                      
+| 11: #ty #e1 #e2 #Hind1 #Hind2
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     cases Hind1
+     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1: cases (exec_expr ge en m e1)
+          [ 2: #error #_ @SimFail /2 by ex_intro/
+          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
+               normalize nodelta
+               cases (exec_bool_of_val ??)
+               [ 2: #error @SimFail /2 by ex_intro/
+               | 1: * whd in match (m_bind ?????);
+                    [ 2: @SimOk // ]
+                    cases Hind2
+                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+                    | 1: cases (exec_expr ge en m e2)
+                         [ 2: #error #_  @SimFail /2 by ex_intro/
+                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
+                              @SimOk #a2
+                              whd in match (m_bind ?????); //
+     ] ] ] ] ]
+| 12: #ty #e1 #e2 #Hind1 #Hind2
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     cases Hind1
+     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1: cases (exec_expr ge en m e1)
+          [ 2: #error #_ @SimFail /2 by ex_intro/
+          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
+               normalize nodelta
+               cases (exec_bool_of_val ??)
+               [ 2: #error @SimFail /2 by ex_intro/
+               | 1: * whd in match (m_bind ?????);
+                    [ 1: @SimOk // ]
+                    cases Hind2
+                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+                    | 1: cases (exec_expr ge en m e2)
+                         [ 2: #error #_  @SimFail /2 by ex_intro/
+                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
+                              @SimOk #a2
+                              whd in match (m_bind ?????); //
+     ] ] ] ] ]
+| 13: #ty #sizeof_ty
+     whd in match (exec_expr ge ???);    
+     whd in match (exec_expr ge' ???);
+     @SimOk //
+| 14: #ty #e #ty' #fld #Hind
+     whd in match (exec_lvalue' ge ????);
+     whd in match (exec_lvalue' ge' ????);
+     whd in match (typeof ?);
+     cases ty' in Hind;
+     [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
+     | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
+     normalize nodelta #Hind
+     try (@SimFail /2 by ex_intro/)
+     whd in match (exec_lvalue ????);
+     whd in match (exec_lvalue ????);     
+     cases Hind
+     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1,3: cases (exec_lvalue' ge en m e ?)
+         [ 2,4: #error #_ @SimFail /2 by ex_intro/
+         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
+     ] ]
+| 15: #ty #l #e #Hind
+     whd in match (exec_expr ge ???);
+     whd in match (exec_expr ge' ???);
+     cases Hind
+     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
+     | 1: cases (exec_expr ge en m e)
+        [ 2: #error #_ @SimFail /2 by ex_intro/
+        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
+     ] ]
+| 16: *
+  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
+  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
+  #ty normalize in ⊢ (% → ?);
+  [ 1,2: #_ @SimOk #a normalize //
+  | 3,4,13: #H @(False_ind … H)
+  | *: #_ @SimFail /2 by ex_intro/
+  ]
+] qed. *)
+
+(*
+lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
+related_globals ? fundef_switch_removal ge ge' →
+∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
+#ge #ge' #en #m #Hrelated #args
+elim args
+[ 1: /3/
+| 2: #hd #tl #Hind normalize
+     elim (sim_related_globals ge ge' en m Hrelated)
+     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
+     cases (exec_expr ge en m hd)
+     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
+     | 1: * #val_hd #trace_hd normalize nodelta
+          cases Hind
+          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
+          | 1: cases (exec_exprlist ge en m tl)
+               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
+               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
+                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
+                    cases Hexec_hd
+                    [ 2: * #error #Habsurd destruct (Habsurd)
+                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
+] ] ] ] qed.
+*)
+
+(* 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
+qed.
+
+(* Similar stuff for fundefs *)
+lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
+* // qed.
+
+(*
 lemma expr_fresh_lift : 
   ∀e,u,id. 
@@ -828 +2601 @@
 cases (leb p p') normalize nodelta
 [ 1: @H2 | 2: @H1 ]
-qed. 
-
+qed. *)
 
 lemma while_fresh_lift : ∀e,s,u.
    fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
-#e #s #u normalize #Hfresh_expr
-elim (max_of_statement s (an_identifier SymbolTag one)) #p 
-#Hfresh_p
-@expr_fresh_lift
-[ 2: //
-| 1: @Hfresh_expr ]
-qed.
-
-(*    
-theorem switch_removal_correction : ∀ge, ge', u.
-  related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' →
-  ∀s1, s1', tr, s2. 
+#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
+cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
+cases (leb e s) try /2/
+qed.
+
+(*
+lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
+#e0 #s0 #us0 normalize 
+cases (switch_removal s0 us0) * #body #newvars #u' normalize //
+qed.*)
+
+lemma dowhile_fresh_lift : ∀e,s,u.
+   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
+#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
+cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
+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).
+#e0 #s0 #us0 normalize
+cases (switch_removal s0 us0) * #body #newvars #u' normalize //
+qed.*)
+
+lemma for_fresh_lift : ∀cond,step,body,u. 
+  fresh_for_statement step u → 
+  fresh_for_statement body u → 
+  fresh_for_expression cond u → 
+  fresh_for_statement (Sfor Sskip cond step body) u.
+#cond #step #body #u
+whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
+cases (max_of_statement step) #s
+cases (max_of_statement body) #b
+cases (max_of_expr cond) #c
+whd in match (max_of_statement Sskip); 
+>(max_id_commutative least_identifier)
+>max_id_one_neutral normalize nodelta
+normalize elim u #u
+cases (leb s b) cases (leb c b) cases (leb c s) try /2/
+qed.
+
+(*
+lemma for_commute : ∀e,stm1,stm2,u,uA.
+   (uA=\snd  (switch_removal stm1 u)) → 
+   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
+#e #stm1 #stm2 #u #uA #HuA
+whd in match (sw_rem (Sfor ????) u);
+whd in match (switch_removal ??);   
+destruct
+normalize in match (\snd (switch_removal Sskip u));
+whd in match (sw_rem stm1 u);
+cases (switch_removal stm1 u)
+* #stm1' #fresh_vars #uA normalize nodelta
+whd in match (sw_rem stm2 uA);
+cases (switch_removal stm2 uA)
+* #stm2' #fresh_vars2 #uB normalize nodelta
+//
+qed.*)
+
+(*
+lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem 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 ??);     
+     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 ??);
+     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.
+*)
+
+(*
+lemma sw_rem_commute : ∀stm,u.
+  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
+#stm #u whd in match (sw_rem stm u); // qed.
+*)
+
+lemma fresh_for_statement_inv : 
+  ∀u,s. fresh_for_statement s u →
+        match u with
+        [ mk_universe p ⇒ le (p0 one) p ]. 
+* #p #s whd in match (fresh_for_statement ??);
+cases (max_of_statement s) #s
+normalize /2/ qed.
+
+lemma fresh_for_Sskip :
+  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
+#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
+
+lemma fresh_for_Sbreak :
+  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
+#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
+
+lemma fresh_for_Scontinue :
+  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
+#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.
+
+(*
+lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
+#s #u elim (switch_removal s u) * #res #fvs #u'
+%{res} %{fvs} %{u'} //
+qed.
+
+lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
+#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
+%{res} %{fvs} %{u'} //
+qed.
+*)
+
+lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
+#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
+#s #lab #u' %{s} %{lab} %{u'} //
+qed.
+
+(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
+lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
+* * *
+[ 1,5,9: #H @(False_ind … (H (refl ??)))
+| *: #_ normalize @refl ]
+qed.
+
+lemma exec_expr_int : ∀ge,e,m,expr.
+    (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)).
+#ge #e #m #expr cases (exec_expr ge e m expr)
+[ 2: #error %2 #sz #n #tr % #H destruct (H)
+| 1: * #val #trace cases val
+     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
+     | 3: #fl | 4: | 5: #ptr ]
+     %2 #sz #n #tr % #H destruct (H)
+] qed.
+
+(*
+lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
+  exec_expr ge e m cond = OK ? 〈v,tr〉 → 
+  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
+  exec_expr ge' e m cond = OK ? 〈v,tr〉.
+#ge #ge' #e #m #cond #v #tr #H *
+[ 1: #Hsim >(Hsim ? H) //
+| 2: * #error >H #Habsurd destruct (Habsurd) ]
+qed. *)
+
+(*
+lemma switch_simulation :
+∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
+ switch_cont_sim k k' →
+ (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
+ fresh_for_statement (Sswitch cond switchcases) u →
+ ∃tr'.
+ (eventually ge'
+  (λs2':state
+   .switch_state_sim
+    (State f
+     (seq_of_labeled_statement (select_switch condsz condval switchcases))
+     (Kswitch k) e m) s2')
+  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
+  tr').
+#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
+whd in match (sw_rem (Sswitch cond switchcases) u);
+whd in match (switch_removal (Sswitch cond switchcases) u);
+cases switchcases in Hfresh;
+[ 1: #default_statement #Hfresh_for_default
+     whd in match (switch_removal_branches ??);
+     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
+     elim (switch_removal_eq default_statement u)
+     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
+     normalize nodelta
+     cut (u' = (\snd (switch_removal default_statement u)))
+     [ 1: >Hdefault_statement_eq // ] #Heq_u'
+     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
+     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
+     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
+     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
+     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
+     normalize nodelta
+     whd in match (simplify_switch (Expr ??) ?? uv2);
+     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
+     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
+     -Hfreshness #Heq_uv3
+     normalize nodelta whd in match (add_starting_lbl_list ????);
+     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
+     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
+     -Hfreshness #Heq_uv4
+     normalize nodelta
+     @(eventually_later ge' ?? E0)
+     whd in match (exec_step ??);
+     %{(State (function_switch_removal f)
+          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
+          (Kseq
+          (Ssequence
+            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
+            (Slabel exit_label Sskip))
+          k') e m)} @conj try //
+     @(eventually_later ge' ?? E0)
+     whd in match (exec_step ??);
+     
+@chthulhu | @chthulhu
+qed. *)
+
+
+
+(* Main theorem. To be ported and completed to memory injections. TODO *)
+(*
+theorem switch_removal_correction : ∀ge, ge'.
+  related_globals ? fundef_switch_removal ge ge' →
+  ∀s1, s1', tr, s2.
   switch_state_sim s1 s1' →
   exec_step ge s1 = Value … 〈tr,s2〉 →
   eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
-#ge #ge' #u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
+#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
 inversion Hsim_state
 [ 1: (* regular state *)
-  #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_
+  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
+  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_
+
+  lapply (sim_related_globals ge ge' e m Hrelated) *
+  #Hexpr_related #Hlvalue_related
   >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
-  cases s in Hus_fresh;
+  cases s in Hu_fresh Heq_env;
+  
+
+theorem switch_removal_correction : ∀ge, ge'.
+  related_globals ? fundef_switch_removal ge ge' →
+  ∀s1, s1', tr, s2.
+  switch_state_sim s1 s1' →
+  exec_step ge s1 = Value … 〈tr,s2〉 →
+  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
+#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
+inversion Hsim_state
+[ 1: (* regular state *)
+  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
+  lapply (sim_related_globals ge ge' e m Hrelated) *
+  #Hexpr_related #Hlvalue_related
+  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
+  cases s in Hu_fresh Heq_env;
   (* Perform the intros for the statements*)
-  [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
+  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
   | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
   | 14: #lab | 15: #cost #body ]
-  #Hus_fresh
+  #Hu_fresh #Heq_env
   [ 1: (* Skip *)
     whd in match (sw_rem ??);
     inversion Hsim_cont normalize nodelta
     [ 1: #Hk #Hk' #_ #Hexec_step
-         @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e))))
-         [ 1: whd in match (exec_step ??); >fn_return_simplify ]
+         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
          cases (fn_return f) in Hexec_step;
          [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain
          | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
          normalize nodelta
-         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct //
+         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
+                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @conj try //
+                normalize in Heq_env; destruct (Heq_env)
+                %3 //
+(*                cut (blocks_of_env e = blocks_of_env e')
+                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
+                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
+                #Heq >Heq %3 // *)
          | *: #H destruct (H) ]
-    | 2: #s0 #k0 #k0' #us0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
+    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
          whd in match (ret ??) in Heq; destruct (Heq)
          @(eventually_now ????) whd in match (exec_step ??);
-         %{(State (\fst  (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try //
-         %1{uf us0 uk} //
-         >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk'
-         whd in ⊢ (% → ?); * #_ //
-    | 3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
+         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
+         %1 try //   
+    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
          @(eventually_now ????) whd in match (exec_step ??);
          whd in match (ret ??) in Heq; destruct (Heq)
-         %{(State (\fst  (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try //
-         >while_commute %1{uf us0 uk} //
-         [ 1: @while_fresh_lift assumption
-         | 2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ]
-    | 4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
+         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
+         >while_commute %1 try //
+    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
          @(eventually_now ????) whd in match (exec_step ??);
- 
-         
-         
-         [ 1: @uk
-         | 2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ]
-                  
-         whd
-         normalize
-         
-         cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0))
-         [ 1: whd in match (sw_rem (Swhile ??) ?);
-              whd in match (switch_removal ??);
-         whd in match (exec_step ??);
-
-(* foireux pour le (Expr (Econst_int sz n) ?) *)
-lemma convert :
-∀uv. 
-  ∀sz,n,sl. 
-    seq_of_labeled_statements (select_switch sz n sl)
-    ~~~u
-    let 〈exit_label, uv1〉            ≝ fresh ? uv in    
-    let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in    
-    Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip)
-    
-
-lemma convert :
-∀f,cond,ls,k,ge,e,m.
-  ∀t.
-    ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 →
-    ∀uf,us.
-     fresh_for_function f uf →
-     fresh_for_statement (Sswitch cond ls) us →   
-    ∃s',k'.
-     (exec_plus ge 
-        E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m)
-        t s')
-     ∧ switch_cont_sim k k'
-     ∧ switch_state_sim 
-        (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m)
-        s'.
-#f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus
-whd in match (sw_rem ??);
-whd in match (switch_removal ??);
-check eq_ind
-
-
-
-whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec;
-[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ]
-* #cond_val #cond_trace 
-whd in match (bindIO ??????);
-cases cond_val
-[ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ]
-[ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ]
-normalize nodelta #Heq whd in match (ret ??) in Heq;
-
-
-    
-    
-      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
-      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
-                    | _ ⇒ Wrong ??? (msg TypeMismatch) ]    
-
-theorem step_with_labels : ∀ge,ge'.
-  related_globals ? label_fundef ge ge' →
-  state_with_labels s1 s1' →
-  exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 →
-  (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch 
-  (exec_step ge st (Sswitch e ls)
+         lapply (Hexpr_related e0)
+         cases (exec_expr ge e m e0) in Heq;
+         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
+         | 1: * #b #tr whd in match (m_bind ?????); #Heq
+              *
+              [ 2: * #error #Habsurd destruct (Habsurd)
+              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
+                   whd in match (bindIO ??????);
+                   cases (exec_bool_of_val b (typeof e0)) in Heq;
+                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
+                        whd in match (bindIO ??????);
+                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
+                             @conj // >dowhile_commute %1 try //
+                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
+                             @conj // %1{us} try //
+                             @(fresh_for_Sskip … Hus_fresh)
+                        ] ] ] ]
+    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
+         @(eventually_now ????) whd in match (exec_step ??);
+         whd in match (ret ??) in Heq; destruct
+         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
+         @conj try // %1{u} try //
+    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
+         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
+         destruct (Heq)
+         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
+         @conj try // %1
+         [ 2: @swc_for3 //
+         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
+    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
+         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
+         destruct (Heq)
+         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
+         @conj try // <(for_commute ??? u uA) try // %1
+         [ 2: assumption
+         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
+    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
+         #Heq @(eventually_now ????) whd in match (exec_step ??);
+         destruct (Heq)
+         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
+         %1{u} //
+    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
+         @(eventually_now ????) whd in match (exec_step ??);
+         >fn_return_simplify cases (fn_return f) in Heq;
+         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
+         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
+         normalize nodelta
+         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
+              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
+              @conj try // %3 destruct //
+         | *: #H destruct (H) ]     
+     ]
+  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
+       whd in match (exec_step ??);
+       cases lhs in Hu_fresh Heq; #lhs #lhs_type
+       cases (Hlvalue_related lhs lhs_type)
+       whd in match (exec_lvalue ge e m (Expr ??));
+       whd in match (exec_lvalue ge' e m (Expr ??));
+       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
+       cases (exec_lvalue' ge e m lhs lhs_type)
+       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
+       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
+            whd in match (m_bind ?????);
+            cases (Hexpr_related rhs)
+            [ 2: * #error #Hfail >Hfail #_
+                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+            | 1: cases (exec_expr ge e m rhs)
+                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
+                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
+                      whd in match (bindIO ??????) in ⊢ (% → % → %);
+                      cases (opt_to_io io_out io_in ???) 
+                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
+                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
+                           %{(State (function_switch_removal f) Sskip k' e mem)}
+                           whd in match (bindIO ??????); @conj //
+                           %1{u} try // @(fresh_for_Sskip … Hfresh)
+       ] ] ] ]
+   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
+        whd in match (exec_step ??);
+        cases (Hexpr_related func) in Heq;
+        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 1: cases (exec_expr ge e m func)
+             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
+                  whd in match (m_bind ?????); normalize nodelta
+                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
+                  #Hexprlist_sim cases (Hexprlist_sim args)
+                  [ 2: * #error #Hfail >Hfail
+                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+                  | 1: cases (exec_exprlist ge e m args)
+                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
+                            whd in match (bindIO ??????) in ⊢ (% → %);
+                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
+                            cases (find_funct clight_fundef ge fval)
+                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
+                                 whd in match (bindIO ??????) in ⊢ (% → %);
+                                 >fundef_type_simplify
+                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
+                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
+                                      cases retv normalize nodelta
+                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
+                                           %{(Callstate (fundef_switch_removal clfd) values
+                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
+                                           @conj try // %2 try // @swc_call //
+                                      | 2: * #retval_ed #retval_type
+                                           whd in match (exec_lvalue ge ???);
+                                           whd in match (exec_lvalue ge' ???);                                      
+                                           elim (Hlvalue_related retval_ed retval_type)
+                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
+                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
+                                                     destruct (Habsurd)
+                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
+                                                     whd in match (m_bind ?????) in ⊢ (% → %);
+                                                     #Heq destruct (Heq)
+                                                     %{(Callstate (fundef_switch_removal clfd) values
+                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
+                                                               (function_switch_removal f) e k') m)}
+                                                     @conj try //
+                                                     %2 @swc_call //
+                                ] ] ] ]
+                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
+                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
+       ] ] ] ] ]
+   | 4: (* Ssequence *) normalize nodelta
+        whd in match (ret ??) in ⊢ (% → ?); #Heq
+        @(eventually_now ????) 
+        %{(State (function_switch_removal f)
+                 (\fst (\fst (switch_removal stm1 u)))
+                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
+        @conj
+        [ 2: destruct (Heq) %1
+             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
+             | 2: @swc_seq try // @switch_removal_fresh 
+                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
+        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
+             cases (switch_removal stm1 u)
+             * #stm1' #fresh_vars #u' normalize nodelta
+             cases (switch_removal stm2 u')
+             * #stm2' #fresh_vars2 #u'' normalize nodelta
+             whd in match (exec_step ??);
+             destruct (Heq) @refl
+        ]
+   | 5: (* If-then-else *) normalize nodelta
+        whd in match (ret ??) in ⊢ (% → ?); #Heq
+        @(eventually_now ????) whd in match (sw_rem ??);
+        whd in match (switch_removal ??);
+        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
+        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
+        whd in match (exec_step ??);
+        cases (Hexpr_related cond) in Heq;
+        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 1: cases (exec_expr ge e m cond)
+             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
+                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
+                  cases (exec_bool_of_val condval (typeof cond))
+                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
+                       destruct (Heq_condval) whd in match (bindIO ??????);
+                       normalize nodelta
+                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
+                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
+                           [ 1: >Hiftrue_eq normalize // ]
+                           #Hrewrite >Hrewrite %1
+                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
+                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
+                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
+                           [ 1: >Hiffalse_eq // ]
+                           #Hrewrite >Hrewrite %1 try //
+                           cut (uA = (\snd (switch_removal iftrue u)))
+                           [ 1: >Hiftrue_eq //
+                           | 2: #Heq_uA >Heq_uA
+                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
+                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
+       ] ] ] ] ]
+   | 6: (* While loop *) normalize nodelta
+        whd in match (ret ??) in ⊢ (% → ?); #Heq
+        @(eventually_now ????) whd in match (sw_rem ??);
+        whd in match (switch_removal ??);
+        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
+        whd in match (exec_step ??);
+        cases (Hexpr_related cond) in Heq;
+        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+        | 1: cases (exec_expr ge e m cond)
+             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
+                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
+                  cases (exec_bool_of_val condval (typeof cond))
+                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
+                       destruct (Heq_condval) whd in match (bindIO ??????);
+                       normalize nodelta
+                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
+                            cut (body' = (\fst (\fst (switch_removal body u))))
+                            [ 1: >Hbody_eq // ]
+                            #Hrewrite >Hrewrite %1
+                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
+                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
+                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
+                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
+        ] ] ] ]
+   | 7: (* Dowhile loop *) normalize nodelta
+        whd in match (ret ??) in ⊢ (% → ?); #Heq
+        @(eventually_now ????) whd in match (sw_rem ??);
+        whd in match (switch_removal ??);
+        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
+        whd in match (exec_step ??);
+        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
+        try //
+        cut (body' = (\fst (\fst (switch_removal body u))))
+        [ 1: >Hbody_eq // ]
+        #Hrewrite >Hrewrite %1
+        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
+        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
+   | 8: (* For loop *) normalize nodelta
+        whd in match (ret ??) in ⊢ (% → ?); #Heq
+        @(eventually_now ????) whd in match (sw_rem ??);
+        whd in match (switch_removal ??);
+        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
+        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
+              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
+              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
+              whd in match (exec_step ??);
+              cases (Hexpr_related cond)
+              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+              | 1: cases (exec_expr ge e m cond)
+                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
+                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
+                        cases (exec_bool_of_val condval (typeof cond))
+                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
+                             destruct (Heq_condval)
+                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
+                                  try //
+                                  cut (body' = (\fst (\fst (switch_removal body uA))))
+                                  [ 1: >Hbody_eq // ]
+                                  #Hrewrite >Hrewrite
+                                  cut (uA = (\snd (switch_removal step u)))
+                                  [ 1: >Hstep_eq // ] #HuA
+                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
+                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
+                                  [ 1: >HuA @switch_removal_fresh assumption
+                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
+                                       [ >Hstep_eq // ]
+                                       #Hstep >Hstep @swc_for2 try assumption
+                                       @for_fresh_lift try assumption ]
+                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
+                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
+               ] ] ] ]
+        | 2: #Heq
+             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
+             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
+             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
+             whd in match (exec_step ??);
+             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
+             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
+             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
+             whd in match (ret ??); destruct (Heq)
+             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
+             @conj try //
+             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
+             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
+             <for_commute [ 2: >Hstep_eq // ]
+             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
+             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
+             @swc_seq try // @for_fresh_lift
+             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
+             >HuA_eq @switch_removal_fresh assumption       
+       ]
+   | 9: (* break *) normalize nodelta
+        inversion Hsim_cont
+        [ 1: #Hk #Hk' #_        
+        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
+        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
+        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
+        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
+        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
+        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
+        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
+        normalize nodelta #H try (destruct (H))
+        whd in match (ret ??) in H; destruct (H)
+        @(eventually_now ????)
+        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
+        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
+    | 10: (* Continue *) normalize nodelta
+        inversion Hsim_cont
+        [ 1: #Hk #Hk' #_        
+        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
+        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
+        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
+        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
+        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
+        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
+        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
+        normalize nodelta #H try (destruct (H))
+        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
+        destruct (H)
+        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
+        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
+             >while_commute %1{u0} try assumption
+        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
+             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+             | 1: * #condval #trace whd in match (m_bind ?????);
+                  #Heq * 
+                  [ 2: * #error #Habsurd destruct (Habsurd)
+                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
+                       whd in match (bindIO ??????);
+                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
+                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
+                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
+                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)} 
+                                 @conj try // >dowhile_commute %1{u0} assumption
+                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
+                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
+             ] ] ]
+        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
+             try // @(fresh_for_Scontinue … Hfor_fresh)
+        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
+             @conj try // %1{u0}
+             elim (substatement_fresh … Hfor_fresh) * * try //
+             #HSskip #Hcond #Hstep #Hbody
+             @swc_for3 assumption
+        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
+             %1{u} try //
+        ]
+    | 11: (* Sreturn *) normalize nodelta #Heq
+          @(eventually_now ????)
+          whd in match (exec_step ??) in Heq ⊢ %;
+          cases retval in Heq; normalize nodelta
+          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
+               whd in match (ret ??) in ⊢ (% → %);
+               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
+               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
+               #H destruct (H)
+               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
+               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
+          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
+               [ 1: #_ #Habsurd destruct (Habsurd)
+               | 2: #_ elim (Hexpr_related expr)
+                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
+                    | 1: cases (exec_expr ??? expr)
+                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
+                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
+                              #Hrewrite >Hrewrite
+                              whd in match (m_bind ?????); whd in match (m_bind ?????);
+                              #Heq destruct (Heq)
+                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
+                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
+         ] ] ] ]
+    | 12: (* Sswitch. Main proof case. *) normalize nodelta
+          (* Case analysis on the outcome of the tested expression *)
+          cases (exec_expr_int ge e m cond)
+          [ 2: cases (exec_expr ge e m cond)
+               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
+               | 1: * #val #trace cases val
+                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
+                    whd in match (m_bind ?????);
+                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
+                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
+          ]
+          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
+          whd in match (m_bind ?????); #Heq
+          destruct (Heq)
+          @eventually_later
+          whd in match (sw_rem (Sswitch cond switchcases) u);
+          whd in match (switch_removal (Sswitch cond switchcases) u);
+          elim (switch_removal_branches_eq switchcases u)
+          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
+          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
+          [ 1: >Hsrb_eq // ] #Huv1_eq
+          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
+          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
+          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
+          whd in match (simplify_switch ???);
+          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
+          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
+          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)          
+          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
+          #Huv4_eq
+          whd in match (exec_step ??);
+          %{(State (function_switch_removal f)
+                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
+                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
+          %{E0} @conj try @refl
+          %{tr} normalize in match (eq ???); @conj try //
+          (* execute the conditional *)
+          @eventually_later
+          (* lift the result of the previous case analysis from [ge] to [ge'] *)
+          whd in match (exec_step ??);
+          whd in match (exec_lvalue ????);
+          
+          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
+          
+  *)
   
-  
-   ∃tr',s2'. plus ge' s1' tr' s2' ∧
-             trace_with_extra_labels tr tr' ∧
-             state_with_labels s2 s2').
-
-
-*)
-