diff --git a/List.lp b/List.lp
index 45d8ccf..c507c55 100644
--- a/List.lp
+++ b/List.lp
@@ -1069,7 +1069,7 @@ end;
 opaque symbol mem_head [a] beq (x:τ a) l :
   π (beq x x = true) → π (∈ beq x (x ⸬ l)) ≔
 begin
-  assume a beq x l hrefl; simplify; rewrite hrefl; apply ⊤ᵢ;
+  assume a beq x l hrefl; rewrite hrefl; apply ⊤ᵢ;
 end;
 
 opaque symbol mem_tail [a] (beq: τ a → τ a → 𝔹) (n m: τ a) (l: 𝕃 a) : 
diff --git a/Z.lp b/Z.lp
index f46909b..c695737 100644
--- a/Z.lp
+++ b/Z.lp
@@ -501,7 +501,7 @@ symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔
 begin
   assume x y z;
   rewrite ≐_sub; rewrite .[x in _ = x] ≐_sub;
-  simplify; rewrite distr_—_+; rewrite .[— y + — z] +_com;
+  rewrite distr_—_+; rewrite .[— y + — z] +_com;
   rewrite +_assoc; rewrite left +_assoc z (— z) (— y);
   rewrite -_same z; reflexivity;
 end;
@@ -545,7 +545,7 @@ end;
 symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔
 begin
   assume x y a; simplify; assume H; rewrite ≐_sub;
-  simplify; rewrite +_assoc; rewrite .[y + a] +_com;
+  rewrite +_assoc; rewrite .[y + a] +_com;
   rewrite distr_—_+; rewrite left +_assoc a (— a) (— y);
   rewrite -_same; rewrite left +_assoc;
   simplify; rewrite left ≐_sub; refine H;