diff --git a/coq/AffineValidation.v b/coq/AffineValidation.v
index 25ff67670bda564c8fdd46e1b230284c40071d8d..9d7026c7e4420a08a890ef9653267c5ea9ffacc9 100644
--- a/coq/AffineValidation.v
+++ b/coq/AffineValidation.v
@@ -5,234 +5,6 @@ Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.Real
 Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
 Require Import Flover.IntervalValidation Flover.RealRangeArith.
 
-Lemma usedVars_eq_compat e1 e2:
-  Q_orderedExps.eq e1 e2 ->
-  NatSet.eq (usedVars e1) (usedVars e2).
-Proof.
-  intros Heq.
-  unfold Q_orderedExps.eq in Heq.
-  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
-  - apply Nat.compare_eq in Heq.
-    now rewrite Heq.
-  - now set_tac.
-  - simpl.
-    reflexivity.
-  - set_tac.
-  - specialize (IHc e6).
-    specialize (IHc0 Heq).
-    apply NatSet.eq_leibniz in IHc.
-    apply NatSet.eq_leibniz in IHc0.
-    simpl.
-    now rewrite IHc, IHc0.
-  - specialize (IHc e6).
-    specialize (IHc0 Heq).
-    apply NatSet.eq_leibniz in IHc.
-    apply NatSet.eq_leibniz in IHc0.
-    simpl.
-    now rewrite IHc, IHc0.
-  - specialize (IHc e6).
-    specialize (IHc0 Heq).
-    apply NatSet.eq_leibniz in IHc.
-    apply NatSet.eq_leibniz in IHc0.
-    simpl.
-    now rewrite IHc, IHc0.
-  - specialize (IHc e6).
-    specialize (IHc0 Heq).
-    apply NatSet.eq_leibniz in IHc.
-    apply NatSet.eq_leibniz in IHc0.
-    simpl.
-    now rewrite IHc, IHc0.
-  - specialize (IHc e3).
-    specialize (IHc0 e4).
-    specialize (IHc1 Heq).
-    apply NatSet.eq_leibniz in IHc.
-    apply NatSet.eq_leibniz in IHc0.
-    apply NatSet.eq_leibniz in IHc1.
-    simpl.
-    now rewrite IHc, IHc0, IHc1.
-  - simpl.
-    now apply IHc.
-  - simpl in e5.
-    rewrite andb_false_iff in e5.
-    destruct e5.
-    + apply Ndec.Pcompare_Peqb in e8.
-      congruence.
-    + apply N.compare_eq in Heq; subst.
-      rewrite N.eqb_refl in H; congruence.
-Qed.
-
-Lemma usedVars_toREval_toRExp_compat e:
-  usedVars (toREval (toRExp e)) = usedVars e.
-Proof.
-  induction e; simpl; set_tac.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2, IHe3.
-Qed.
-
-Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
-  Q_orderedExps.eq e1 e2 ->
-  validRanges e1 A E Gamma fBits ->
-  validRanges e2 A E Gamma fBits.
-Proof.
-  intros Heq.
-  unfold Q_orderedExps.eq in Heq.
-  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
-  - simpl.
-    intros [_ validr1].
-    repeat split; auto.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    apply Nat.compare_eq in Heq.
-    rewrite <- Heq.
-    intuition.
-  - intros [_ validr1].
-    repeat split; auto.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      unfold Q_orderedExps.exprCompare.
-      rewrite e3; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite e3; auto.
-  - simpl in e3.
-    rewrite andb_false_iff in e3.
-    destruct e3.
-    + apply Ndec.Pcompare_Peqb in e6.
-      congruence.
-    + apply N.compare_eq in Heq; subst.
-      rewrite N.eqb_refl in H; congruence.
-  - intros valid1; destruct valid1 as [validsub1 validr1].
-    specialize (IHc Heq validsub1).
-    split; auto.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e5; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite e5; auto.
-  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
-    specialize (IHc e6 validsub1).
-    specialize (IHc0 Heq validsub1').
-    repeat split; auto; try congruence.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e6; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite Heq, e6; auto.
-  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
-    specialize (IHc e6 validsub1).
-    specialize (IHc0 Heq validsub1').
-    repeat split; auto; try congruence.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e6; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite Heq, e6; auto.
-  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
-    specialize (IHc e6 validsub1).
-    specialize (IHc0 Heq validsub1').
-    repeat split; auto; try congruence.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e6; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite Heq, e6; auto.
-  - intros valid1; destruct valid1 as [[Hdiv [validsub1 validsub1']] validr1].
-    specialize (IHc e6 validsub1).
-    specialize (IHc0 Heq validsub1').
-    repeat split; auto.
-    {
-      intros Hrefl; specialize (Hdiv Hrefl).
-      intros iv2 err Hfind.
-      erewrite FloverMapFacts.P.F.find_o with (y := e12) in Hfind.
-      eapply Hdiv; eauto.
-      now rewrite Q_orderedExps.exprCompare_eq_sym.
-    }
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e6; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite Heq, e6; auto.
-  - intros valid1; destruct valid1 as [[validsub1 [validsub1' validsub1'']] validr1].
-    specialize (IHc e3 validsub1).
-    specialize (IHc0 e4 validsub1').
-    specialize (IHc1 Heq validsub1'').
-    repeat split; auto; try congruence.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e3, e4, Heq; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite Heq, e3, e4; auto.
-  - intros valid1; destruct valid1 as [validsub1 validr1].
-    specialize (IHc Heq validsub1).
-    split; auto.
-    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
-    exists iv, err, vR.
-    intuition.
-    + rewrite <- Hfind.
-      symmetry.
-      apply FloverMapFacts.P.F.find_o.
-      simpl.
-      rewrite e5; auto.
-    + erewrite expr_compare_eq_eval_compat; eauto.
-      rewrite Q_orderedExps.exprCompare_eq_sym.
-      simpl.
-      rewrite e5; auto.
-  - simpl in e5.
-    rewrite andb_false_iff in e5.
-    destruct e5.
-    + apply Ndec.Pcompare_Peqb in e8.
-      congruence.
-    + apply N.compare_eq in Heq; subst.
-      rewrite N.eqb_refl in *; congruence.
-Qed.
-
 Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
   let new_iv := toIntv new_af in
   if isSupersetIntv new_iv intv then
@@ -723,28 +495,6 @@ Definition affine_dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResul
          E v = Some vR /\
          af_evals (afQ2R af) vR map1.
 
-Definition affine_fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
-  forall v,
-    NatSet.In v fVars ->
-    exists vR, E v = Some vR /\
-          (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
-
-Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
-  forall v, NatSet.In v S ->
-       exists m: mType, Gamma v = Some m.
-
-Lemma contained_flover_map_none (e: expr Q) (expmap1: FloverMap.t (affine_form Q)) expmap2:
-  contained_flover_map expmap1 expmap2 ->
-  FloverMap.find e expmap2 = None ->
-  FloverMap.find e expmap1 = None.
-Proof.
-  intros cont Hfound1.
-  unfold contained_flover_map in cont.
-  destruct (FloverMap.find (elt:=affine_form Q) e expmap1) eqn: Heq; auto.
-  apply cont in Heq.
-  congruence.
-Qed.
-
 Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma fBits:
   (exists map af vR aiv aerr,
       FloverMap.find e A = Some (aiv, aerr) /\
@@ -822,8 +572,8 @@ Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
   validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
   affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
   NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
-  affine_fVars_P_sound fVars E P ->
-  affine_vars_typed (NatSet.union fVars dVars) Gamma ->
+  fVars_P_sound fVars E P ->
+  vars_typed (NatSet.union fVars dVars) Gamma ->
   exists map2 af vR aiv aerr,
     contained_map map1 map2 /\
     contained_flover_map iexpmap exprAfs /\
@@ -2169,93 +1919,6 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
   | Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
   end.
 
-Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m n c fVars dVars outVars:
-  ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
-  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
-  ~ (n ∈ fVars ∪ dVars) ->
-  eval_expr E Gamma fBits e vR REAL ->
-  eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
-Proof.
-  intros Hssa Hsub Hnotin Heval.
-  eapply eval_expr_ignore_bind; [auto |].
-  edestruct ssa_inv_let; eauto.
-Qed.
-
-Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma fBits vR' m n c fVars dVars outVars:
-  ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
-  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
-  ~ (n ∈ fVars ∪ dVars) ->
-  validRanges e A E Gamma fBits ->
-  validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma) fBits.
-Proof.
-  intros Hssa Hsub Hnotin Hranges.
-  induction e.
-  - split; auto.
-    destruct Hranges as [_ [iv [err [vR Hranges]]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-  - split; auto.
-    destruct Hranges as [_ [iv [err [vR Hranges]]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-  - simpl in Hsub.
-    destruct Hranges as [Hunopranges Hranges].
-    specialize (IHe Hsub Hunopranges).
-    split; auto.
-    destruct Hranges as [iv [err [vR Hranges]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-    rewrite usedVars_toREval_toRExp_compat; auto.
-  - simpl in Hsub.
-    assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac.
-    assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac).
-    destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
-    specialize (IHe1 Hsub1 Hranges1).
-    specialize (IHe2 Hsub2 Hranges2).
-    simpl.
-    repeat split; auto.
-    destruct Hranges as [iv [err [vR Hranges]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-    simpl.
-    repeat rewrite usedVars_toREval_toRExp_compat; auto.
-  - simpl in Hsub.
-    assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac.
-    assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac).
-    assert (NatSet.Subset (usedVars e3) (fVars ∪ dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
-    destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
-    specialize (IHe1 Hsub1 Hranges1).
-    specialize (IHe2 Hsub2 Hranges2).
-    specialize (IHe3 Hsub3 Hranges3).
-    simpl.
-    repeat split; auto.
-    destruct Hranges as [iv [err [vR Hranges]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-    simpl.
-    repeat rewrite usedVars_toREval_toRExp_compat; auto.
-  - simpl in Hsub.
-    destruct Hranges as [Hranges' Hranges].
-    specialize (IHe Hsub Hranges').
-    split; auto.
-    destruct Hranges as [iv [err [vR Hranges]]].
-    exists iv, err, vR; intuition.
-    eapply swap_Gamma_eval_expr.
-    eapply Rmap_updVars_comm.
-    eapply eval_expr_ssa_extension; try eassumption.
-    rewrite usedVars_toREval_toRExp_compat; auto.
-Qed.
-
 Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond) fBits
       fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
   (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
@@ -2266,8 +1929,8 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond) fBi
   ssa c (NatSet.union fVars dVars) outVars ->
   affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
   NatSet.Subset (NatSet.diff (Commands.freeVars c) dVars) fVars ->
-  affine_fVars_P_sound fVars E P ->
-  affine_vars_typed (NatSet.union fVars dVars) Gamma ->
+  fVars_P_sound fVars E P ->
+  vars_typed (NatSet.union fVars dVars) Gamma ->
   exists map2 af vR aiv aerr,
     contained_map map1 map2 /\
     contained_flover_map iexpmap exprAfs /\
@@ -2286,7 +1949,7 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond) fBi
 Proof.
   revert E Gamma dVars iexpmap inoise exprAfs noise map1.
   induction c; intros * visitedExpr Hnoise Hmapvalid valid_bounds_cmd
-                        Hssa dvars_valid Hsubset fvars_valid vars_typed; simpl in valid_bounds_cmd.
+                        Hssa dvars_valid Hsubset fvars_valid vtyped; simpl in valid_bounds_cmd.
   - destruct (FloverMap.find e A) eqn: Hares__e; try congruence.
     destruct p as (aiv__e, aerr__e).
     destruct aiv__e as (elo, ehi).
@@ -2390,13 +2053,13 @@ Proof.
         apply a_no_dVar.
         rewrite NatSet.add_spec; auto. }
     }
-    assert (affine_vars_typed (fVars ∪ NatSet.add n dVars) (updDefVars n REAL Gamma)) as H4''.
+    assert (vars_typed (fVars ∪ NatSet.add n dVars) (updDefVars n REAL Gamma)) as H4''.
     {
       intros x x_contained.
       set_tac.
       destruct x_contained as [x_free | x_def].
       {
-        destruct (vars_typed x) as [m_x Gamma_x]; try set_tac.
+        destruct (vtyped x) as [m_x Gamma_x]; try set_tac.
         exists m_x.
         unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
         rewrite Nat.eqb_eq in eq_case.
@@ -2407,7 +2070,7 @@ Proof.
         set_tac.
         destruct x_def as [x_n | x_def]; subst.
         - exists REAL; unfold updDefVars; rewrite Nat.eqb_refl; auto.
-        - destruct x_def. destruct (vars_typed x) as [m_x Gamma_x].
+        - destruct x_def. destruct (vtyped x) as [m_x Gamma_x].
           + rewrite NatSet.union_spec; auto.
           + exists m_x.
             unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
@@ -2415,7 +2078,7 @@ Proof.
             congruence.
       }
     }
-    assert (affine_fVars_P_sound fVars (updEnv n vR E) P) as H4'''.
+    assert (fVars_P_sound fVars (updEnv n vR E) P) as H4'''.
     {
       intros v0 mem_fVars.
       unfold updEnv.
diff --git a/coq/Expressions.v b/coq/Expressions.v
index 6668c69a20b203432bf6dd76b2effd14a1698e78..a9d409565743c53eb554d75b869c673fc433506d 100644
--- a/coq/Expressions.v
+++ b/coq/Expressions.v
@@ -484,6 +484,14 @@ Proof.
       hnf; intros; eapply no_usedVar;
         set_tac.
 Qed.
+
+Lemma Rmap_updVars_comm Gamma n m:
+  forall x,
+    updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
+Proof.
+  unfold updDefVars, toRMap; simpl.
+  intros x; destruct (x =? n); try auto.
+Qed.
 (*
 (**
 Analogous lemma for unary expressions.
diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v
index 020ad2b2ea07f3ba2fcb53a154a5f819cfd98454..7ce6c8d740b5db7a796e6d56c5d4127a8817a13d 100644
--- a/coq/Infra/ExpressionAbbrevs.v
+++ b/coq/Infra/ExpressionAbbrevs.v
@@ -89,6 +89,70 @@ Proof.
   - rewrite e5, e8; auto.
 Qed.
 
+Lemma usedVars_eq_compat e1 e2:
+  Q_orderedExps.eq e1 e2 ->
+  NatSet.eq (usedVars e1) (usedVars e2).
+Proof.
+  intros Heq.
+  unfold Q_orderedExps.eq in Heq.
+  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
+  - apply Nat.compare_eq in Heq.
+    now rewrite Heq.
+  - now set_tac.
+  - simpl.
+    reflexivity.
+  - set_tac.
+  - specialize (IHc e6).
+    specialize (IHc0 Heq).
+    apply NatSet.eq_leibniz in IHc.
+    apply NatSet.eq_leibniz in IHc0.
+    simpl.
+    now rewrite IHc, IHc0.
+  - specialize (IHc e6).
+    specialize (IHc0 Heq).
+    apply NatSet.eq_leibniz in IHc.
+    apply NatSet.eq_leibniz in IHc0.
+    simpl.
+    now rewrite IHc, IHc0.
+  - specialize (IHc e6).
+    specialize (IHc0 Heq).
+    apply NatSet.eq_leibniz in IHc.
+    apply NatSet.eq_leibniz in IHc0.
+    simpl.
+    now rewrite IHc, IHc0.
+  - specialize (IHc e6).
+    specialize (IHc0 Heq).
+    apply NatSet.eq_leibniz in IHc.
+    apply NatSet.eq_leibniz in IHc0.
+    simpl.
+    now rewrite IHc, IHc0.
+  - specialize (IHc e3).
+    specialize (IHc0 e4).
+    specialize (IHc1 Heq).
+    apply NatSet.eq_leibniz in IHc.
+    apply NatSet.eq_leibniz in IHc0.
+    apply NatSet.eq_leibniz in IHc1.
+    simpl.
+    now rewrite IHc, IHc0, IHc1.
+  - simpl.
+    now apply IHc.
+  - simpl in e5.
+    rewrite andb_false_iff in e5.
+    destruct e5.
+    + apply Ndec.Pcompare_Peqb in e8.
+      congruence.
+    + apply N.compare_eq in Heq; subst.
+      rewrite N.eqb_refl in H; congruence.
+Qed.
+
+Lemma usedVars_toREval_toRExp_compat e:
+  usedVars (toREval (toRExp e)) = usedVars e.
+Proof.
+  induction e; simpl; set_tac.
+  - now rewrite IHe1, IHe2.
+  - now rewrite IHe1, IHe2, IHe3.
+Qed.
+
 Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
 Module FloverMapFacts := OrdProperties (FloverMap).
 
@@ -132,6 +196,18 @@ Proof.
     auto.
 Qed.
 
+Lemma contained_flover_map_none (V: Type) (e: expr Q) (expmap1: FloverMap.t V) expmap2:
+  contained_flover_map expmap1 expmap2 ->
+  FloverMap.find e expmap2 = None ->
+  FloverMap.find e expmap1 = None.
+Proof.
+  intros cont Hfound1.
+  unfold contained_flover_map in cont.
+  destruct (FloverMap.find e expmap1) eqn: Heq; auto.
+  apply cont in Heq.
+  congruence.
+Qed.
+
 Definition toRBMap (bMap:FloverMap.t N) : expr R -> option N :=
   let elements := FloverMap.elements (elt:=N) bMap in
   fun (e:expr R) =>
diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v
index 2f8469b3da9b036b062470f5792a6102545b69a5..c729426507c91542a951146287b3d4b543941373 100644
--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -373,14 +373,6 @@ Proof.
     simpl in *; lra.
 Qed.
 
-Lemma Rmap_updVars_comm Gamma n m:
-  forall x,
-    updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
-Proof.
-  unfold updDefVars, toRMap; simpl.
-  intros x; destruct (x =? n); try auto.
-Qed.
-
 Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
   forall Gamma E fVars dVars outVars P fBits,
     ssa f (NatSet.union fVars dVars) outVars ->
diff --git a/coq/RealRangeArith.v b/coq/RealRangeArith.v
index 0ee4801c02c675503db06f1bbbfa4515053c60b8..80bf7b68cc7c859eeb8751e1b5709d4034e9f4ab 100644
--- a/coq/RealRangeArith.v
+++ b/coq/RealRangeArith.v
@@ -1,9 +1,9 @@
 From Coq
-     Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz.
+     Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz Recdef.
 
 From Flover
      Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
-     Infra.Ltacs Infra.RealSimps Typing IntervalArithQ IntervalArith Commands.
+     Infra.Ltacs Infra.RealSimps Typing ssaPrgs IntervalArithQ IntervalArith Commands.
 
 Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
   forall v, NatSet.In v dVars ->
@@ -155,4 +155,243 @@ Proof.
       * eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
   - destruct valid1.
     eapply validRanges_swap; eauto.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
+  Q_orderedExps.eq e1 e2 ->
+  validRanges e1 A E Gamma fBits ->
+  validRanges e2 A E Gamma fBits.
+Proof.
+  intros Heq.
+  unfold Q_orderedExps.eq in Heq.
+  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
+  - simpl.
+    intros [_ validr1].
+    repeat split; auto.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    apply Nat.compare_eq in Heq.
+    rewrite <- Heq.
+    intuition.
+  - intros [_ validr1].
+    repeat split; auto.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      unfold Q_orderedExps.exprCompare.
+      rewrite e3; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite e3; auto.
+  - simpl in e3.
+    rewrite andb_false_iff in e3.
+    destruct e3.
+    + apply Ndec.Pcompare_Peqb in e6.
+      congruence.
+    + apply N.compare_eq in Heq; subst.
+      rewrite N.eqb_refl in H; congruence.
+  - intros valid1; destruct valid1 as [validsub1 validr1].
+    specialize (IHc Heq validsub1).
+    split; auto.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e5; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite e5; auto.
+  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
+    specialize (IHc e6 validsub1).
+    specialize (IHc0 Heq validsub1').
+    repeat split; auto; try congruence.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e6; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite Heq, e6; auto.
+  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
+    specialize (IHc e6 validsub1).
+    specialize (IHc0 Heq validsub1').
+    repeat split; auto; try congruence.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e6; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite Heq, e6; auto.
+  - intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
+    specialize (IHc e6 validsub1).
+    specialize (IHc0 Heq validsub1').
+    repeat split; auto; try congruence.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e6; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite Heq, e6; auto.
+  - intros valid1; destruct valid1 as [[Hdiv [validsub1 validsub1']] validr1].
+    specialize (IHc e6 validsub1).
+    specialize (IHc0 Heq validsub1').
+    repeat split; auto.
+    {
+      intros Hrefl; specialize (Hdiv Hrefl).
+      intros iv2 err Hfind.
+      erewrite FloverMapFacts.P.F.find_o with (y := e12) in Hfind.
+      eapply Hdiv; eauto.
+      now rewrite Q_orderedExps.exprCompare_eq_sym.
+    }
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e6; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite Heq, e6; auto.
+  - intros valid1; destruct valid1 as [[validsub1 [validsub1' validsub1'']] validr1].
+    specialize (IHc e3 validsub1).
+    specialize (IHc0 e4 validsub1').
+    specialize (IHc1 Heq validsub1'').
+    repeat split; auto; try congruence.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e3, e4, Heq; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite Heq, e3, e4; auto.
+  - intros valid1; destruct valid1 as [validsub1 validr1].
+    specialize (IHc Heq validsub1).
+    split; auto.
+    destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
+    exists iv, err, vR.
+    intuition.
+    + rewrite <- Hfind.
+      symmetry.
+      apply FloverMapFacts.P.F.find_o.
+      simpl.
+      rewrite e5; auto.
+    + erewrite expr_compare_eq_eval_compat; eauto.
+      rewrite Q_orderedExps.exprCompare_eq_sym.
+      simpl.
+      rewrite e5; auto.
+  - simpl in e5.
+    rewrite andb_false_iff in e5.
+    destruct e5.
+    + apply Ndec.Pcompare_Peqb in e8.
+      congruence.
+    + apply N.compare_eq in Heq; subst.
+      rewrite N.eqb_refl in *; congruence.
+Qed.
+
+Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma fBits vR' m n c fVars dVars outVars:
+  ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
+  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
+  ~ (n ∈ fVars ∪ dVars) ->
+  validRanges e A E Gamma fBits ->
+  validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma) fBits.
+Proof.
+  intros Hssa Hsub Hnotin Hranges.
+  induction e.
+  - split; auto.
+    destruct Hranges as [_ [iv [err [vR Hranges]]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+  - split; auto.
+    destruct Hranges as [_ [iv [err [vR Hranges]]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+  - simpl in Hsub.
+    destruct Hranges as [Hunopranges Hranges].
+    specialize (IHe Hsub Hunopranges).
+    split; auto.
+    destruct Hranges as [iv [err [vR Hranges]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+    rewrite usedVars_toREval_toRExp_compat; auto.
+  - simpl in Hsub.
+    assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac.
+    assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac).
+    destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
+    specialize (IHe1 Hsub1 Hranges1).
+    specialize (IHe2 Hsub2 Hranges2).
+    simpl.
+    repeat split; auto.
+    destruct Hranges as [iv [err [vR Hranges]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+    simpl.
+    repeat rewrite usedVars_toREval_toRExp_compat; auto.
+  - simpl in Hsub.
+    assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac.
+    assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac).
+    assert (NatSet.Subset (usedVars e3) (fVars ∪ dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
+    destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
+    specialize (IHe1 Hsub1 Hranges1).
+    specialize (IHe2 Hsub2 Hranges2).
+    specialize (IHe3 Hsub3 Hranges3).
+    simpl.
+    repeat split; auto.
+    destruct Hranges as [iv [err [vR Hranges]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+    simpl.
+    repeat rewrite usedVars_toREval_toRExp_compat; auto.
+  - simpl in Hsub.
+    destruct Hranges as [Hranges' Hranges].
+    specialize (IHe Hsub Hranges').
+    split; auto.
+    destruct Hranges as [iv [err [vR Hranges]]].
+    exists iv, err, vR; intuition.
+    eapply swap_Gamma_eval_expr.
+    eapply Rmap_updVars_comm.
+    eapply eval_expr_ssa_extension; try eassumption.
+    rewrite usedVars_toREval_toRExp_compat; auto.
+Qed.
diff --git a/coq/RealRangeValidator.v b/coq/RealRangeValidator.v
index 5ffac7214808600edc7cf66082963d921e6bbeba..9b78d5a7b01bbcf4bb57a5d48382954d68a7a993 100644
--- a/coq/RealRangeValidator.v
+++ b/coq/RealRangeValidator.v
@@ -45,8 +45,8 @@ Proof.
     assert (1 > 0)%nat as Hinoise by omega.
     eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
     assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
-    assert (affine_fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
-    assert (affine_vars_typed (usedVars e ∪ dVars) Gamma) as Hvarstyped
+    assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
+    assert (vars_typed (usedVars e ∪ dVars) Gamma) as Hvarstyped
         by exact H3.
     specialize (sound_affine e A P (usedVars e) dVars E Gamma fBits
                              exprAfs noise iexpmap inoise imap
@@ -95,8 +95,8 @@ Proof.
             congruence).
     assert (1 > 0)%nat as Hinoise by omega.
     eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
-    assert (affine_fVars_P_sound fVars E P) as HfVars by exact H2.
-    assert (affine_vars_typed (fVars ∪ dVars) Gamma) as Hvarstyped
+    assert (fVars_P_sound fVars E P) as HfVars by exact H2.
+    assert (vars_typed (fVars ∪ dVars) Gamma) as Hvarstyped
         by exact H3.
     specialize (sound_affine f A P fBits fVars dVars outVars E Gamma
                              exprAfs noise iexpmap inoise imap
diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v
index 01f81480ff0a2cb85c121c6837d36627e5cc6a57..f6d9c6d1c8d0687ab3feb9141b42d08a9c3ed5c4 100644
--- a/coq/ssaPrgs.v
+++ b/coq/ssaPrgs.v
@@ -210,6 +210,18 @@ Proof.
   set_tac.
 Qed.
 
+Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m n c fVars dVars outVars:
+  ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
+  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
+  ~ (n ∈ fVars ∪ dVars) ->
+  eval_expr E Gamma fBits e vR REAL ->
+  eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
+Proof.
+  intros Hssa Hsub Hnotin Heval.
+  eapply eval_expr_ignore_bind; [auto |].
+  edestruct ssa_inv_let; eauto.
+Qed.
+
 (*
 Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
   (forall n, E1 n = E2 n)->