diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v
index 97bf92eb35a5df8e86fb076b13c15562479131de..67cb44d19d7eaa49c32a75f5438aa42411678253 100644
--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
@@ -6,23 +6,21 @@
    encoded in the analysis result. The validator is used in the file
    CertificateChecker.v to build the complete checker.
  **)
-Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
-               Coq.QArith.Qreals Coq.micromega.Psatz Coq.Reals.Reals.
-Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps
-               Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps
-               Daisy.Infra.Ltacs Daisy.Environments
-               Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
+From Coq
+     Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
+     micromega.Psatz Reals.Reals.
+From Daisy
+     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
+     Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
+     ErrorBounds.
 
 (** Error bound validator **)
 Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
-         (typeMap:exp Q -> option mType) (* derived types for e *)
+         (typeMap:DaisyMap.t mType) (* derived types for e *)
          (A:analysisResult) (* encoded result of Daisy *)
          (dVars:NatSet.t) (* let-bound variables encountered previously *):=
-  let (intv, err) := (A e) in
-  let mopt := typeMap e in
-  match mopt with
-  | None => false
-  | Some m =>
+  match DaisyMap.find e A, DaisyMap.find e typeMap with
+  | Some (intv, err), Some m =>
     if (Qleb 0 err) (* encoding soundness: errors are positive *)
     then
       match e with (* case analysis for the expression *)
@@ -34,60 +32,74 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
        Qleb (maxAbs intv * (mTypeToQ m)) err
       |Unop Neg e1 =>
        if (validErrorbound e1 typeMap A dVars)
-       then Qeq_bool err (snd (A e1))
+       then
+         match DaisyMap.find e1 A with
+         | Some (iv_e1, err1) => Qeq_bool err err1
+         | None => false
+         end
        else false
       |Unop Inv e1 => false
       |Binop b e1 e2 =>
        if ((validErrorbound e1 typeMap A dVars)
              && (validErrorbound e2 typeMap A dVars))
        then
-         let (ive1, err1) := A e1 in
-         let (ive2, err2) := A e2 in
-         let errIve1 := widenIntv ive1 err1 in
-         let errIve2 := widenIntv ive2 err2 in
-         let upperBoundE1 := maxAbs ive1 in
-         let upperBoundE2 := maxAbs ive2 in
-         match b with
-         | Plus =>
-           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
-         | Sub =>
-           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
-         | Mult =>
-           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
-         | Div =>
-           if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
-               ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
-           then
-             let upperBoundInvE2 := maxAbs (invertIntv ive2) in
-             let minAbsIve2 := minAbs (errIve2) in
-             let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
-             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
-           else false
+         match DaisyMap.find e1 A, DaisyMap.find e2 A with
+         | Some (ive1, err1), Some (ive2, err2) =>
+           let errIve1 := widenIntv ive1 err1 in
+           let errIve2 := widenIntv ive2 err2 in
+           let upperBoundE1 := maxAbs ive1 in
+           let upperBoundE2 := maxAbs ive2 in
+           match b with
+           | Plus =>
+             Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
+           | Sub =>
+             Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
+           | Mult =>
+             Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
+           | Div =>
+             if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
+                 ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
+             then
+               let upperBoundInvE2 := maxAbs (invertIntv ive2) in
+               let minAbsIve2 := minAbs (errIve2) in
+               let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
+               Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
+             else false
+           end
+         | _, _ => false
          end
        else false
       |Downcast m1 e1 =>
        if validErrorbound e1 typeMap A dVars
        then
-         let (ive1, err1) := A e1 in
-         let errIve1 := widenIntv ive1 err1 in
-         (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
+         match DaisyMap.find e1 A with
+         | Some (ive1, err1) =>
+          let errIve1 := widenIntv ive1 err1 in
+          (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
+         | None => false
+         end
        else
          false
       end
     else false
+  | _, _ => false
   end.
 
 (** Error bound command validator **)
 Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *)
-         (typeMap:exp Q -> option mType) (* inferred types *)
+         typeMap (* inferred types *)
          (A:analysisResult) (* Daisy's encoded result *)
          (dVars:NatSet.t) (* defined variables *)
          : bool :=
   match f with
   |Let m x e g =>
-   if ((validErrorbound e typeMap A dVars) && (Qeq_bool (snd (A e)) (snd (A (Var Q x)))))
-   then validErrorboundCmd g typeMap A (NatSet.add x dVars)
-   else false
+   match DaisyMap.find e A, DaisyMap.find (Var Q x) A with
+     | Some (iv_e, err_e), Some (iv_x, err_x) =>
+       if ((validErrorbound e typeMap A dVars) && (Qeq_bool err_e err_x))
+       then validErrorboundCmd g typeMap A (NatSet.add x dVars)
+       else false
+     | _,_ => false
+   end
   |Ret e => validErrorbound e typeMap A dVars
   end.
 
diff --git a/coq/Infra/Ltacs.v b/coq/Infra/Ltacs.v
index 0fcf10be6fd0cb82865062504bf352eb44601b0a..0889636ed4ac41bf39603e29c572d018d315688b 100644
--- a/coq/Infra/Ltacs.v
+++ b/coq/Infra/Ltacs.v
@@ -91,6 +91,15 @@ Ltac match_simpl :=
   repeat match_factorize;
   try pair_factorize.
 
+Ltac bool_factorize :=
+  match goal with
+  | [H: _ = true |- _] => andb_to_prop H
+  end.
+
+Ltac Daisy_compute :=
+  repeat
+    (match_simpl || bool_factorize).
+
 (* Ltac destruct_if := *)
 (*   match goal with *)
 (*   | [H: if ?c then ?a else ?b = _ |- _ ] => *)
diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v
index 15907a91d59993bd70a7f83b2e840823c486cfc6..d0fb567191b507fe1ffbc69a88a6bd0d36e6cf99 100644
--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -105,22 +105,20 @@ Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err:
 Proof.
   induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
   - subst.
-    match_simpl.
+    Daisy_compute.
     destruct (var mem dVars) eqn:?; set_tac; try congruence.
-    andb_to_prop approx_true; unfold isSupersetIntv.
+    Daisy_compute.
+    unfold isSupersetIntv.
     apply andb_prop_intro; split;
         apply Is_true_eq_left; auto.
-  - match_simpl.
-    andb_to_prop approx_true.
+  - Daisy_compute; try congruence.
     apply IHf; try auto.
     set_tac.
-  - match_simpl.
-    andb_to_prop approx_true.
+  - Daisy_compute; try congruence.
     destruct H.
     + apply IHf1; try auto; set_tac.
     + apply IHf2; try auto; set_tac.
-  - match_simpl.
-    andb_to_prop approx_true.
+  - Daisy_compute; try congruence.
     apply IHf; try auto; set_tac.
 Qed.
 
@@ -142,20 +140,16 @@ Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
   (ivhi_e2 < 0) \/ (0 < ivlo_e2).
 Proof.
   intros A_eq validBounds; cbn in *.
-  match_simpl.
-  andb_to_prop validBounds.
-  repeat match_simpl.
-  andb_to_prop R.
-  unfold isSupersetIntv in *; simpl in *.
+  Daisy_compute; try congruence.
   apply le_neq_bool_to_lt_prop; auto.
 Qed.
 
 Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
   forall v, NatSet.In v dVars ->
-       exists vR ivlo ivhi err,
+       exists vR iv err,
          E v =  Some vR /\
-         DaisyMap.find (Var Q v) A = Some ((ivlo, ivhi), err) /\
-         (Q2R ivlo <= vR <= Q2R ivhi)%R.
+         DaisyMap.find (Var Q v) A = Some (iv, err) /\
+         (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 
 Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
   forall v,
@@ -167,6 +161,11 @@ Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
   forall v, NatSet.In v S ->
        exists m :mType, Gamma v = Some m.
 
+Ltac kill_trivial_exists :=
+  match goal with
+  | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ /\ _] => exists i, e
+  end.
+
 Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
         fVars dVars (E:env) Gamma:
     validIntervalbounds f A P dVars = true ->
@@ -174,22 +173,23 @@ Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
     NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
     fVars_P_sound fVars E P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
-    exists ivlo ivhi err vR,
-      DaisyMap.find f A = Some ((ivlo, ivhi), err) /\
+    exists iv err vR,
+      DaisyMap.find f A = Some (iv, err) /\
       eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
-      (Q2R ivlo <= vR <= Q2R ivhi)%R.
+      (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 Proof.
   induction f;
     intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
     cbn in *.
-  - match_simpl.
+  - Daisy_compute.
     destruct (NatSet.mem n dVars) eqn:?; simpl in *.
     + destruct (valid_definedVars n)
-        as [vR [ivlo_n [ivhi_n [err_n [env_valid [map_n bounds_valid]]]]]];
+        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
         try set_tac.
       rewrite map_n in *.
       inversion Heqo; subst.
-      exists ivlo_n, ivhi_n, e; eexists; split; [auto| split; try eauto ].
+      kill_trivial_exists.
+      eexists; split; [auto| split; try eauto ].
       eapply Var_load; simpl; try auto.
       destruct (types_defined n) as [m type_m];
         set_tac.
@@ -199,43 +199,42 @@ Proof.
       assert (NatSet.In n fVars) by set_tac.
       andb_to_prop valid_bounds.
       canonize_hyps; simpl in *.
-      exists (fst i), (snd i), e; eexists; split;
-        [destruct i; auto | split].
+      kill_trivial_exists.
+      eexists; split; [auto | split].
       * econstructor; try eauto.
-        destruct (types_defined n) as [m type_m]; set_tac.
+        destruct (types_defined n) as [m type_m];
+          set_tac.
         match_simpl; auto.
       * lra.
-  - match_simpl.
-    andb_to_prop valid_bounds.
-    canonize_hyps; simpl in *.
-    exists (fst i), (snd i), e, (perturb (Q2R v) 0).
-    split; [destruct i; auto| split].
+  - Daisy_compute; canonize_hyps; simpl in *.
+    kill_trivial_exists.
+    exists (perturb (Q2R v) 0).
+    split; [auto| split].
     + econstructor; try eauto. apply Rabs_0_equiv.
     + unfold perturb; simpl; lra.
-  - match_simpl.
-    andb_to_prop valid_bounds.
-    match_simpl.
-    destruct IHf as [ivlo_f [ivhi_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]];
+  - Daisy_compute; simpl in *; try congruence.
+    destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]];
       try auto.
-    destruct u; try andb_to_prop R.
-    + exists (fst i), (snd i), e, (evalUnop Neg vF); split;
-        [destruct i; auto | split ;
+    inversion iveq_f; subst.
+    destruct u; try andb_to_prop R; simpl in *.
+    + kill_trivial_exists.
+      exists (evalUnop Neg vF); split;
+        [auto | split ;
                             [econstructor; eauto | ]].
-      canonize_hyps; simpl in *.
+      canonize_hyps.
       rewrite Q2R_opp in *.
-      destruct valid_bounds_f.
-      inversion iveq_f; subst; simpl in *; lra.
-    + inversion iveq_f; subst; simpl in *.
-      rename L0 into nodiv0.
+      simpl; lra.
+    + rename L0 into nodiv0.
       apply le_neq_bool_to_lt_prop in nodiv0.
-      exists (fst i), (snd i), e, (perturb (evalUnop Inv vF) 0); split;
+      kill_trivial_exists.
+      exists (perturb (evalUnop Inv vF) 0); split;
         [destruct i; auto | split].
       * econstructor; eauto; try apply Rabs_0_equiv.
         (* Absence of division by zero *)
         hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
                rewrite Q2R0_is_0 in nodiv0; lra.
       * canonize_hyps.
-        pose proof (interval_inversion_valid ((Q2R ivlo_f),(Q2R ivhi_f)) (a :=vF)) as inv_valid.
+        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
          unfold invertInterval in inv_valid; simpl in *.
          rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra].
          destruct inv_valid; try auto.
@@ -245,7 +244,7 @@ Proof.
            - rewrite Q2R_inv; try auto.
              destruct nodiv0; try lra.
              hnf; intros.
-             assert (0 < Q2R (ivhi_f))%R.
+             assert (0 < Q2R (snd iv_f))%R.
              { eapply Rlt_le_trans.
                apply Qlt_Rlt in H1.
                rewrite <- Q2R0_is_0.
@@ -258,7 +257,7 @@ Proof.
            - rewrite <- Q2R_inv; try auto.
              hnf; intros.
              destruct nodiv0; try lra.
-             assert (Q2R ivlo_f < 0)%R.
+             assert (Q2R (fst iv_f) < 0)%R.
              { eapply Rle_lt_trans.
                Focus 2.
                rewrite <- Q2R0_is_0;
@@ -267,23 +266,23 @@ Proof.
              }
              rewrite <- Q2R0_is_0 in H3.
              apply Rlt_Qlt in H3. lra. }
-  - match_simpl.
-    andb_to_prop valid_bounds.
-    repeat match_simpl.
-    destruct IHf1 as [ivlo_f1 [ivhi_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]];
+  - Daisy_compute; try congruence.
+    destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]];
       try auto; set_tac.
-    destruct IHf2 as [ivlo_f2 [ivhi_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]];
+    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
       try auto; set_tac.
     assert (M0 = join M0 M0) as M0_join by (cbv; auto);
       rewrite M0_join.
-    exists (fst i), (snd i), e, (perturb (evalBinop b vF1 vF2) 0);
+    kill_trivial_exists.
+    exists (perturb (evalBinop b vF1 vF2) 0);
       split; [destruct i; auto | ].
     inversion env1; inversion env2; subst.
       destruct b; simpl in *.
     * split;
         [econstructor; try congruence; apply Rabs_0_equiv | ].
-      pose proof (interval_addition_valid ((Q2R ivlo_f1), Q2R ivhi_f1)
-                                          (Q2R ivlo_f2, Q2R ivhi_f2)) as valid_add.
+      pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
+                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
+        as valid_add.
       specialize (valid_add vF1 vF2 valid_f1 valid_f2).
       unfold isSupersetIntv in R.
       andb_to_prop R.
@@ -293,8 +292,8 @@ Proof.
       unfold perturb. lra.
     * split;
         [econstructor; try congruence; apply Rabs_0_equiv |].
-      pose proof (interval_subtraction_valid (Q2R ivlo_f1, Q2R ivhi_f1)
-                                             (Q2R ivlo_f2, Q2R ivhi_f2))
+      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
+                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_sub.
       specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
       unfold isSupersetIntv in R.
@@ -306,8 +305,8 @@ Proof.
       unfold perturb; lra.
     * split;
         [ econstructor; try congruence; apply Rabs_0_equiv |].
-      pose proof (interval_multiplication_valid (Q2R ivlo_f1, Q2R ivhi_f1)
-                                                (Q2R ivlo_f2, Q2R ivhi_f2))
+      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
+                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_mul.
       specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
       unfold isSupersetIntv in R.
@@ -325,19 +324,19 @@ Proof.
       { hnf; intros.
         destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
       { pose proof (interval_division_valid (a:=vF1) (b:=vF2)
-                                            (Q2R ivlo_f1, Q2R ivhi_f1)
-                                            (Q2R ivlo_f2, Q2R ivhi_f2))
+                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
+                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_div.
         simpl in *.
         destruct valid_div; try auto.
         - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
-        - assert (~ ivhi_f2 == 0).
+        - assert (~ (snd iv_f2) == 0).
           { hnf; intros. destruct L; try lra.
-            assert (0 < ivhi_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
+            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
             lra. }
-          assert (~ ivlo_f2 == 0).
+          assert (~ (fst iv_f2) == 0).
           { hnf; intros; destruct L; try lra.
-            assert (ivlo_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
+            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
             lra. }
           repeat (rewrite <- Q2R_inv in *; try auto).
           repeat rewrite <- Q2R_mult in *.
@@ -348,10 +347,11 @@ Proof.
   - match_simpl.
     andb_to_prop valid_bounds.
     match_simpl.
-    destruct IHf as [ivlo_f [ivhi_f [err_f [vF [env_f [eval_f valid_f]]]]]];
+    destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]];
       try auto.
     inversion env_f; subst.
-    exists (fst i), (snd i), e, (perturb vF 0).
+    kill_trivial_exists.
+    exists (perturb vF 0).
     split; [destruct i; try auto |].
     split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
     unfold isSupersetIntv in *; andb_to_prop R.
@@ -407,20 +407,20 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
     vars_typed (NatSet.union fVars dVars) Gamma ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     validIntervalboundsCmd f A P dVars = true ->
-    exists elo ehi err vR,
-      DaisyMap.find (getRetExp f) A = Some ((elo, ehi), err) /\
+    exists iv_e err_e vR,
+      DaisyMap.find (getRetExp f) A = Some (iv_e, err_e) /\
       bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
-      (Q2R elo <=  vR <= Q2R ehi)%R.
+      (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
 Proof.
   revert Gamma.
   induction f;
     intros *  ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
     cbn in *.
-  - repeat match_simpl. andb_to_prop valid_bounds_f.
+  - Daisy_compute.
     inversion ssa_f; subst.
     canonize_hyps.
     pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
-    destruct validIV_e as [v_lo [v_hi [err_v [v [find_v [eval_e valid_bounds_e]]]]]];
+    destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]];
       try auto.
     { set_tac. repeat split; auto.
       hnf; intros; subst.
@@ -433,7 +433,7 @@ Proof.
         destruct H0; auto.
       * destruct in_set as [? | ?]; try auto; set_tac.
         destruct H as [? | [? ?]]; auto.
-    + edestruct IHf as [ivlo_f [ivhi_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]]];
+    + edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]];
         try eauto.
        eapply ssa_equal_set. symmetry in H. apply H. apply H7.
       * intros v0 mem_v0.
@@ -442,7 +442,7 @@ Proof.
         { rename R1 into eq_lo;
             rename R0 into eq_hi.
           rewrite Nat.eqb_eq in v0_eq; subst.
-          exists v; eexists; eexists; eexists; repeat split; try eauto; lra. }
+          exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. }
         { apply dVars_sound.
           set_tac.
           destruct mem_v0 as [? | [? ?]]; try auto.
@@ -486,12 +486,12 @@ Proof.
         { hnf; intros a_dVar.
           apply a_no_dVar.
           rewrite NatSet.add_spec; auto. }
-      * simpl. exists ivlo_f, ivhi_f, err_f, vR; repeat split; try auto; try lra.
+      * simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra.
         econstructor; try eauto.
         eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
         intros n1; erewrite Rmap_updVars_comm; eauto.
   - unfold validIntervalboundsCmd in valid_bounds_f.
     pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
-    destruct valid_iv_e as [?[?[?[? [? [? ?]]]]]]; try auto.
+    destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto.
     simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
 Qed.
\ No newline at end of file
diff --git a/coq/attic/Typing.v b/coq/attic/Typing_old.v
similarity index 100%
rename from coq/attic/Typing.v
rename to coq/attic/Typing_old.v