diff --git a/src/bitvector.lean b/src/bitvector.lean
index cfa9feb..778fa67 100644
--- a/src/bitvector.lean
+++ b/src/bitvector.lean
@@ -43,10 +43,13 @@ def of_int (sz:size) : ℤ → bitvector sz
 | x@(int.neg_succ_of_nat p) :=
   ⟨(((2 ^ sz.val) - p - 1) % (2^sz.val)), ♯⟩
 
+@[simp]
 def all_one (sz:size) : bitvector sz := of_int sz (all_one_nat sz)
 
+@[simp]
 def int_min (sz:size) : bitvector sz := of_int sz (int_min_nat sz)
 
+@[simp]
 def zero (sz:size) : bitvector sz := of_int sz 0
 
 def of_bool (b:bool) : bitvector (size.one) := of_int size.one (cond b 1 0)
diff --git a/src/freevar.lean b/src/freevar.lean
index 6d0cb51..86c07f6 100644
--- a/src/freevar.lean
+++ b/src/freevar.lean
@@ -108,6 +108,7 @@ namespace env
   def add_b (e:env) (name:string) (b:bool):env :=
     {bv := e.bv, b := (λ n, if n = name then some b else e.b n)}
 
+  @[simp]
   mutual def replace_sbv, replace_sb
   with replace_sbv: Π (η:env) {sz:size}, sbitvec sz → sbitvec sz
   | η sz x@(sbitvec.var _ name) :=
@@ -201,8 +202,8 @@ namespace env
     have 0 < sbitvec.sizeof sz x, by apply sbitvec.decr_sbitvec,
     sbool.ult (replace_sbv η x) (replace_sbv η y)
   | η x := x
-  
 
+  @[simp, reducible]
   def replace_valty (η:env) (v:irsem.valty irsem_smt) :=
     match v with
     | irsem.valty.ival sz i p :=
diff --git a/src/smtexpr.lean b/src/smtexpr.lean
index 362c569..2fc2670 100644
--- a/src/smtexpr.lean
+++ b/src/smtexpr.lean
@@ -90,14 +90,19 @@ def of_int (sz:size) : ℤ → sbitvec sz
 | x@(int.neg_succ_of_nat p) :=
   sbitvec.const sz (((2 ^ sz.val) - p - 1) % (2^sz.val))
 
+@[simp]
 def one (sz:size) : sbitvec sz := of_int sz 1
 
+@[simp]
 def zero (sz:size) : sbitvec sz := of_int sz 0
 
+@[simp]
 def intmin (sz:size) : sbitvec sz := of_int sz (int_min_nat sz)
 
+@[simp]
 def intmax (sz:size) : sbitvec sz := of_int sz (int.of_nat ((2^(sz.val-1))-1))
 
+@[simp]
 def uintmax (sz:size) : sbitvec sz := of_int sz (all_one_nat sz)
 
 def of_bool (b:sbool) : sbitvec (size.one) :=
@@ -127,9 +132,11 @@ end
 
 variable {sz:size}
 
+@[simp]
 def mk_zext (m:size) (a:sbitvec sz): sbitvec (sz.add m) :=
   sbitvec.zext (sz.add m) a
 
+@[simp]
 def mk_sext (m:size) (a:sbitvec sz): sbitvec (sz.add m) :=
   sbitvec.sext (sz.add m) a
 
diff --git a/src/spec/closed.lean b/src/spec/closed.lean
index c97aac9..34f93d7 100644
--- a/src/spec/closed.lean
+++ b/src/spec/closed.lean
@@ -63,7 +63,6 @@ lemma closed_b_never_var: ∀ s, ¬ closed_b (sbool.var s)
   unfold env.add_b at H',
   unfold freevar.env.replace_sb at H',
   simp at H',
-  unfold env.replace_sb._match_1 at H',
   cases H'
 end
 
@@ -76,7 +75,6 @@ lemma closed_bv_never_var: ∀ sz s, ¬ closed_bv (sbitvec.var sz s)
   unfold env.add_bv at H',
   unfold freevar.env.replace_sbv at H',
   simp at H',
-  unfold env.replace_sbv._match_1 at H',
   cases H'
 end
 
@@ -169,7 +167,6 @@ lemma closed_b_var_add2: ∀ (η:freevar.env) (v:bool) (s:string),
   simp,
   intros,
   generalize Hb': (η.b s) = b',
-  unfold env.replace_sb._match_1 at *,
   unfold closed_b,
   intros, cases v, refl, refl
 end
@@ -204,14 +201,13 @@ lemma closed_bv_var_add2: ∀ (η:freevar.env) sz v (s:string),
   closed_bv ((η.add_bv s v)⟦sbitvec.var sz s⟧)
 := begin
   unfold env.add_bv,
-  unfold freevar.env.replace_sbv,
-  simp,
   intros,
   generalize Hb': (η.b s) = b',
-  unfold env.replace_sbv._match_1 at *,
   unfold closed_bv,
-  intros, cases v; unfold sbitvec.of_int;
-  unfold freevar.env.replace_sbv
+  intros, cases v;
+  unfold freevar.env.replace_sbv; simp,
+  { unfold sbitvec.of_int, unfold env.replace_sbv },
+  { unfold sbitvec.of_int, unfold env.replace_sbv },
 end
 
 lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b,
@@ -224,18 +220,12 @@ lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b,
   unfold env.add_b,
   unfold env.add_bv,
   simp,
-  unfold freevar.env.replace_valty,
-  unfold freevar.env.replace_sb,
-  unfold freevar.env.replace_sbv,
-  simp,
   split,
   {
-    unfold env.replace_sbv._match_1,
     cases z; unfold sbitvec.of_int;
     unfold freevar.env.replace_sbv
   },
   {
-    unfold env.replace_sb._match_1,
     rw env.replace_sb_of_bool
   }
 end
@@ -289,17 +279,8 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v},
     unfold regfile.apply_to_values at *,
     simp at HC,
     split,
-    {
-      intros,
-      have HC := HC η,
-      injection HC
-    },
-    {
-      intros,
-      have HC := HC η,
-      injection HC,
-      injection h_1
-    }
+    { intros, have HC := HC η, injection HC },
+    { intros, have HC := HC η, injection HC, injection h_1 }
   },
   {
     intros HC η,
@@ -307,11 +288,13 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v},
     have HC1 := HC1 η,
     have HC2 := HC2 η,
     unfold regfile.apply_to_values at *,
-    simp,
+    simp at *,
     rw HC1, rw HC2
   }
 end
 
+
+
 -- TODO 1: Merge closed_b_add_b and closed_bv_add_b into a single
 -- theorem (I tried merging them
 -- but it raised excessive memory consumption error.)
diff --git a/src/spec/customlemmas.lean b/src/spec/customlemmas.lean
index 27daaee..2b731fa 100644
--- a/src/spec/customlemmas.lean
+++ b/src/spec/customlemmas.lean
@@ -34,6 +34,9 @@ def is_poison: irsem.valty irsem_exec → Prop
 set_option eqn_compiler.zeta true
 set_option pp.proofs true
 
+local attribute [simp] option.bind irsem.step irsem.step_bop
+  irsem.bop irsem.bop_ub irsem.irstate.updateub irsem.irstate.updatereg
+
 lemma never_poison:
   ∀ isz name op1 op2 st st' val
     (HSTEP:step st (udiv isz name op1 op2) = some st')
@@ -47,53 +50,31 @@ lemma never_poison:
     injection HNOUB, clear HNOUB,
   cases op2, simp at *,
   {
-    unfold irsem.step at HSTEP,
     cases (irsem.get_value irsem_exec (ub, regs) op1 (ty.int isz)) with val1;
       unfold has_bind.bind at *; unfold option.bind at *,
     injection HSTEP,
-    rw ← HVAL at HSTEP, unfold option.bind at HSTEP,
-    unfold irsem.step_bop at HSTEP,
+    rw ← HVAL at HSTEP, simp at HSTEP,
     cases val1 with isz1 ii1 ip1,
     cases val with isz2 ii2 ip2,
+    simp at HSTEP,
     have HISZDEC:decidable (isz1 = isz2), apply_instance,
-    cases HISZDEC;
-      unfold irsem.step_bop._match_1 at HSTEP;
-      unfold irsem.bop at HSTEP;
-      unfold irsem.step_bop._match_2 at HSTEP;
-      unfold irsem.bop_val at HSTEP,
-    { rw dif_neg at HSTEP, injection HSTEP
-    },
-    {
-      rw (dif_pos HISZDEC) at HSTEP,
+    cases HISZDEC; unfold irsem.bop_val at HSTEP,
+    { rw dif_neg at HSTEP, injection HSTEP },
+    { rw (dif_pos HISZDEC) at HSTEP,
       injection HSTEP with HSTEP', clear HSTEP,
-      generalize HH:
-  (irsem.bop_ub irsem_exec isz1 bopcode.udiv ii1 ip1 (cast (by rw HISZDEC) ii2) ip2)
-    = eub,
-      rw HH at HSTEP',
-      unfold irsem.irstate.updateub at HSTEP',
-      unfold irsem.irstate.updatereg at HSTEP',
-      simp at HSTEP', injection HSTEP' with HUB HREG,
-      cases eub, cases ub; injection HUB,
-      -- now let's unfold irsem.bop_ub.
-      unfold irsem.bop_ub at HH,
-      have HDIV: bop_isdiv bopcode.udiv = tt, by simp,
-      rw (if_pos HDIV) at HH,
-      simp at *,
-      cases ip2,
-      { -- if dividend was poison..
-        unfold_coes at HH, unfold has_and.and at HH,
-        unfold bool_like.and at HH, simp at HH, exfalso, exact HH
-      },
-      {
-        simp
-      }
+      cases ub; cases ip2,
+      any_goals {
+        -- if dividend was poison or previous state was ub..
+        unfold_coes at HSTEP', unfold has_and.and at HSTEP',
+        unfold bool_like.and at HSTEP', simp at HSTEP', injection HSTEP' with HH _,
+        injection HH },
+      { simp }
     }
   },
   {
-    simp at HVAL, unfold irsem.get_value at HVAL,
+    simp at HVAL,
     cases op2,
-    dunfold irsem.get_value._match_1 at HVAL,
-    dunfold irsem.get_value._match_2 at HVAL,
+    unfold irsem.get_value at HVAL,
     have HSZDEC1: decidable (0 < isz), apply_instance,
     cases HSZDEC1,
     { rw (dif_neg HSZDEC1) at HVAL, injection HVAL },
diff --git a/src/spec/freevar.lean b/src/spec/freevar.lean
index c2e293e..864a7b1 100644
--- a/src/spec/freevar.lean
+++ b/src/spec/freevar.lean
@@ -460,11 +460,10 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
     intros,
     unfold freevar.env.replace_sb,
     unfold freevar.env.empty,
-    simp,
-    unfold freevar.env.replace_sb._match_1
+    simp, done
   },
   any_goals {
-    intros b H, unfold freevar.env.replace_sb, rw H, done
+    intros b H, unfold freevar.env.replace_sb, rw H
   },
   any_goals {
     intros b1 b2 H1 H2, unfold freevar.env.replace_sb, rw [H1, H2], done
@@ -486,8 +485,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
     intros,
     unfold freevar.env.replace_sbv,
     unfold freevar.env.empty,
-    simp,
-    unfold freevar.env.replace_sbv._match_1
+    simp, done
   },
   any_goals {
     intros sz v' sz' H,
@@ -505,6 +503,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧
   }
 end
 
+
 lemma env.empty_replace_sb: ∀ (b:sbool), freevar.env.empty⟦b⟧ = b
 := begin
   apply (and.elim_left env.empty_replace)
@@ -530,18 +529,7 @@ lemma env.replace_sb_overflowchk_add: ∀
     sbitvec.overflow_chk @sbitvec.add sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
   intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_add,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_add,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_add
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end
 
 lemma env.replace_sb_overflowchk_sub: ∀
@@ -550,18 +538,7 @@ lemma env.replace_sb_overflowchk_sub: ∀
     sbitvec.overflow_chk @sbitvec.sub sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
   intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_sub,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_sub,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_sub
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end
 
 lemma env.replace_sb_overflowchk_mul: ∀
@@ -570,18 +547,7 @@ lemma env.replace_sb_overflowchk_mul: ∀
     sbitvec.overflow_chk @sbitvec.mul sz2 nsw (η⟦v1⟧) (η⟦v2⟧)
 := begin
   intros, unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_mul,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_mul,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_mul
-  }
+  cases nsw; simp, rw env.replace_sbv_of_int
 end
 
 lemma env.replace_sb_overflowchk_shl: ∀
@@ -591,20 +557,9 @@ lemma env.replace_sb_overflowchk_shl: ∀
 := begin
   intros, unfold sbitvec.shl_overflow_chk,
   unfold sbitvec.overflow_chk,
-  cases nsw; simp; unfold freevar.env.replace_sb,
-  {
-    rw env.replace_sbv_extract,
-    rw env.replace_sbv_shl,
-    repeat { rw env.replace_sbv_mk_zext },
-    unfold sbitvec.zero, rw env.replace_sbv_of_int,
-    rw env.replace_sbv_urem, rw env.replace_sbv_of_int
-  },
-  {
-    rw env.replace_sbv_shl,
-    repeat { rw env.replace_sbv_mk_sext },
-    rw env.replace_sbv_shl,
-    rw env.replace_sbv_urem, rw env.replace_sbv_of_int
-  }
+  cases nsw; simp,
+  { repeat { rw env.replace_sbv_of_int }, tauto },
+  { rw env.replace_sbv_of_int, tauto }
 end
 
 -- irstate
@@ -925,7 +880,7 @@ lemma env.add_b_replace_match: ∀ (η:freevar.env) n b,
   intros,
   unfold freevar.env.replace_sb,
   unfold freevar.env.add_b,
-  simp, unfold freevar.env.replace_sb._match_1
+  simp
 end
 
 lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz,
@@ -934,7 +889,7 @@ lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz,
   intros,
   unfold freevar.env.replace_sbv,
   unfold freevar.env.add_bv,
-  simp, unfold freevar.env.replace_sbv._match_1
+  simp
 end
 
 lemma env.add_bv_replace_sb: ∀ (η:freevar.env) n n' z,
@@ -1297,8 +1252,10 @@ lemma env.not_in_add_bv_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt
       rw ss_snd_ih,
       cases ss_snd_hd with rn v,
       cases v with sz iv pv,
-      rw env.not_in_add_bv_valty_comm,
-      assumption
+      simp,
+      rw env.not_in_add_bv_bv_comm,
+      rw env.not_in_add_bv_b_comm,
+        assumption, assumption
     }
   }
 end
@@ -1332,8 +1289,10 @@ lemma env.not_in_add_b_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt)
       rw ss_snd_ih,
       cases ss_snd_hd with rn v,
       cases v with sz iv pv,
-      rw env.not_in_add_b_valty_comm,
-      assumption
+      simp,
+      rw env.not_in_add_b_bv_comm,
+      rw env.not_in_add_b_b_comm,
+        assumption, assumption
     }
   }
 end
diff --git a/src/spec/lemmas.lean b/src/spec/lemmas.lean
index e6637fb..3d8beec 100644
--- a/src/spec/lemmas.lean
+++ b/src/spec/lemmas.lean
@@ -185,7 +185,7 @@ lemma bvequiv_urem: ∀ (sz:size) (sb:sbitvec sz) eb
   intros,
   apply bv_equiv.urem, assumption, apply bvequiv_from_z,
   { cases sz, unfold_coes, simp, unfold uint_like.from_z, unfold bitvector.ne,
-    unfold bitvector.zero, unfold bitvector.of_int, simp,
+    unfold bitvector.of_int, simp,
     intros H, injection H, simp at h_1, rw nat.mod_pow2 at h_1,
     rw h_1 at sz_property, cases sz_property
   },
diff --git a/src/spec/openprog.lean b/src/spec/openprog.lean
index 01232d1..a9cd90e 100644
--- a/src/spec/openprog.lean
+++ b/src/spec/openprog.lean
@@ -561,8 +561,8 @@ lemma step_replace: ∀ (ss:irstate_smt) (i:instruction)
       have HOPCOND' := apply_some HOPCOND,
       cases HOPCOND' with vopcond' HOPCOND',
       rw HOPCOND',
-      rw get_value_replace,
       unfold option.bind,
+      rw get_value_replace,
       
       cases vop1,
       { rw apply_none at HOP1, rw HOP1, unfold option.bind },