diff --git a/Bool.lp b/Bool.lp
index 1c9bd24..f69aa25 100644
--- a/Bool.lp
+++ b/Bool.lp
@@ -15,8 +15,8 @@ rule τ bool ↪ 𝔹;
 opaque symbol case_𝔹 b : π (b = true ∨ b = false) ≔
 begin
   induction
-  { apply ∨ᵢ₁; reflexivity; }
-  { apply ∨ᵢ₂; reflexivity; }
+  { apply ∨ᵢ₁; reflexivity }
+  { apply ∨ᵢ₂; reflexivity }
 end;
 
 opaque symbol ind_𝔹_eq p b:
@@ -115,12 +115,12 @@ opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔
 begin
   induction
   { induction
-    { assume h; reflexivity }
+    { reflexivity }
     { assume h; apply ⊥ₑ (false≠true h) }
   }
   { induction
     { assume h; apply ⊥ₑ (true≠false h) }
-    { assume h; reflexivity }
+    { reflexivity }
   }
 end;
 
@@ -133,21 +133,11 @@ notation or infix left 20;
 rule true  or _     ↪ true
 with false or $b    ↪ $b;
 
-opaque symbol or_true_lhs [p : 𝔹] :
-  π ((p or true) = true) ≔
-begin
-  induction
-    {reflexivity}
-    {reflexivity}
-end;
+opaque symbol or_true b: π(b or true = true) ≔
+begin induction {reflexivity} {reflexivity} end;
 
-opaque symbol or_false_lhs [p : 𝔹] :
-  π ((p or false) = p) ≔
-begin
-  induction
-    {reflexivity}
-    {reflexivity}
-end;
+opaque symbol or_false b: π(b or false = b) ≔
+begin induction {reflexivity} {reflexivity} end;
 
 // imp
 
@@ -195,15 +185,15 @@ end;
 opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
 begin
   induction
-  { assume q h; apply ∨ᵢ₁; apply ⊤ᵢ; }
-  { assume q h; apply ∨ᵢ₂; apply h; }
+  { assume q h; apply ∨ᵢ₁; apply ⊤ᵢ }
+  { assume q h; apply ∨ᵢ₂; apply h }
 end;
 
 opaque symbol istrue_or [p q : 𝔹] : π(p ∨ q) → π(p or q) ≔
 begin
   induction
-  { assume q h; apply ⊤ᵢ; }
-  { assume q h; apply ∨ₑ h { assume i; apply ⊥ₑ i; } { assume i; apply i; } }
+  { assume q h; apply ⊤ᵢ }
+  { assume q h; apply ∨ₑ h { assume i; apply ⊥ₑ i } { assume i; apply i } }
 end;
 
 opaque symbol orᵢ₁ [p : 𝔹] q : π p → π (p or q) ≔
@@ -231,43 +221,47 @@ end;
 opaque symbol orC p q : π (p or q = q or p) ≔
 begin
     induction
-    { assume q; rewrite or_true_lhs [q]; reflexivity }
-    { assume q; rewrite or_false_lhs [q]; reflexivity }
+    { assume q; rewrite or_true; reflexivity }
+    { assume q; rewrite or_false; reflexivity }
 end;
 
 opaque symbol orA p q r : π ((p or q) or r = p or (q or r)) ≔
 begin
     induction
-    { reflexivity; }
-    { reflexivity; }
+    { reflexivity }
+    { reflexivity }
 end;
 
 // and
 
 symbol and : 𝔹 → 𝔹 → 𝔹;
 
-notation and infix left 7;
+notation and infix left 15;
 
 rule true  and $b    ↪ $b
-with $b    and true  ↪ $b
-with false and _     ↪ false
-with _     and false ↪ false;
+with false and _     ↪ false;
+
+opaque symbol and_true b: π(b and true = b) ≔
+begin induction {reflexivity} {reflexivity} end;
+
+opaque symbol and_false b: π(b and false = false) ≔
+begin induction {reflexivity} {reflexivity} end;
 
 opaque symbol ∧_istrue [p q : 𝔹] : π(p and q) → π(p ∧ q) ≔
 begin
   induction
   { induction
     { assume h; apply ∧ᵢ { apply ⊤ᵢ } { apply ⊤ᵢ } }
-    { assume h; apply ⊥ₑ h; }
+    { assume h; apply ⊥ₑ h }
   }
-  { assume q h; apply ⊥ₑ h; }
+  { assume q h; apply ⊥ₑ h }
 end;
 
 opaque symbol istrue_and [p q : 𝔹] : π(p ∧ q) → π(p and q) ≔
 begin
   induction
-  { assume q h; apply ∧ₑ₂ h; }
-  { assume q h; apply ∧ₑ₁ h; }
+  { assume q h; apply ∧ₑ₂ h }
+  { assume q h; apply ∧ₑ₁ h }
 end;
 
 opaque symbol andᵢ [p q : 𝔹] : π p → π q → π(p and q) ≔
@@ -278,15 +272,15 @@ end;
 opaque symbol andₑ₁ [p q : 𝔹] : π (p and q) → π p ≔
 begin
   induction
-  { assume q i; apply ⊤ᵢ; }
-  { assume q i; apply i; }
+  { assume q i; apply ⊤ᵢ }
+  { assume q i; apply i }
 end;
 
 opaque symbol andₑ₂ [p q : 𝔹] : π (p and q) → π q ≔
 begin
   induction
-  { assume q i; apply i; }
-  { assume q i; apply ⊥ₑ i; }
+  { assume q i; apply i }
+  { assume q i; apply ⊥ₑ i }
 end;
 
 // xorb
diff --git a/Comp.lp b/Comp.lp
index f6c8898..100baaa 100644
--- a/Comp.lp
+++ b/Comp.lp
@@ -74,7 +74,7 @@ with opp Gt ↪ Lt;
 
 opaque symbol opp_idem c : π (opp (opp c) = c) ≔
 begin
-  induction { reflexivity; } { reflexivity; } { reflexivity; }
+  induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
 // Conditional
diff --git a/DepProd.lp b/DepProd.lp
index b32b265..722c8a4 100644
--- a/DepProd.lp
+++ b/DepProd.lp
@@ -19,7 +19,7 @@ rule proj₂ (dpair _ $u) ↪ $u;
 
 opaque symbol η_dprod [a] [p] (e: @DProd a p) :
   π (dpair (proj₁ e) (proj₂ e) = e) ≔
-begin assume a p; induction; assume x u; reflexivity end;
+begin assume a p; induction; reflexivity end;
 
 opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
   π (x = y) → π (proj₁ x = proj₁ y) ≔
diff --git a/ExtraRules.lp b/ExtraRules.lp
index 0259466..b3461c3 100644
--- a/ExtraRules.lp
+++ b/ExtraRules.lp
@@ -1,46 +1,99 @@
 // This module turns proved equalities to rewrite rules
 
+// Bool
+
 require open Stdlib.Bool;
-require Stdlib.Nat as N;
-require open Stdlib.List;
-require Stdlib.Pos as P;
-require Stdlib.Z as Z;
 
-// Bool
+opaque symbol or_true b:π(b or true = true) ≔ or_true b;
+rule _ or true  ↪ true;
 
-rule _ or true  ↪ true
-with $b or false ↪ $b;
+opaque symbol or_false b:π(b or false = b) ≔ or_false b;
+rule $b or false ↪ $b;
+
+opaque symbol and_true b:π(b and true = b) ≔ and_true b;
+rule $b and true ↪ $b;
+
+opaque symbol and_false b:π(b and false = false) ≔ and_false b;
+rule _ and false ↪ false;
 
 // Nat
 
-rule $x N.+ N._0 ↪ $x;
-rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
-rule ($x N.+ $y) N.+ $z ↪ $x N.+ ($y N.+ $z);
-rule $x N.- N._0 ↪ $x;
-rule _ N.* N._0 ↪ N._0;
-rule N.max $x N._0 ↪ $x;
-rule N.max $x $x ↪ $x;
-rule N.min _ N._0 ↪ N._0;
-rule N.min $x $x ↪ $x;
+require open Stdlib.Nat;
+
+opaque symbol addn0 x: π(x + _0 = x) ≔ addn0 x;
+rule $x + _0 ↪ $x;
+
+opaque symbol addnS x y: π(x + y +1 = (x + y) +1) ≔ addnS x y;
+rule $x + $y +1 ↪ ($x + $y) +1;
+
+opaque symbol addnA x y z: π((x + y) + z = x + (y + z)) ≔ addnA x y z;
+rule ($x + $y) + $z ↪ $x + ($y + $z);
+
+opaque symbol subn0 x: π(x - _0 = x) ≔ subn0 x;
+rule $x - _0 ↪ $x;
+
+opaque symbol muln0 x: π(x * _0 = _0) ≔ muln0 x;
+rule _ * _0 ↪ _0;
+
+opaque symbol maxn0 x: π(max x _0 = x) ≔ maxn0 x;
+rule max $x _0 ↪ $x;
+
+opaque symbol maxnn x: π(max x x = x) ≔ maxnn x;
+rule max $x $x ↪ $x;
+
+opaque symbol minn0 x: π(min x _0 = 0) ≔ minn0 x;
+rule min _ _0 ↪ _0;
+
+opaque symbol minnn x: π(min x x = x) ≔ minnn x;
+rule min $x $x ↪ $x;
 
 // List
 
+require open Stdlib.List;
+
+opaque symbol cats0 a (m:𝕃 a): π(m ++ □ = m) ≔ cats0 m;
 rule $m ++ □ ↪ $m;
-rule size ($l ++ $m) ↪ size $l N.+ size $m;
+
+opaque symbol size_cat a (l m:𝕃 a): π(size(l ++ m) = size l + size m) ≔ size_cat l m;
+rule size ($l ++ $m) ↪ size $l + size $m;
+
+opaque symbol catA a (l m n:𝕃 a): π((l ++ m) ++ n = l ++ (m ++ n)) ≔ catA l m n;
 rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
+
+opaque symbol lastl a x e (l:𝕃 a): π(last x (e ⸬ l) = last e l) ≔ lastl l x e;
 rule last _ ($e ⸬ $l) ↪ last $e $l;
+
+opaque symbol nthx□ a (x:τ a) n: π(nth x □ n = x) ≔ nthx□ n x;
 rule nth $x □ _ ↪ $x;
+
+opaque symbol dropx□ a n: π(drop n □ = □ [a]) ≔ dropx□ n;
 rule drop _ □ ↪ □;
+
+opaque symbol taken□ a n: π(take n □ = □ [a]) ≔ taken□ n;
 rule take _ □ ↪ □;
 
 // Pos
 
-rule P.add $x P.H ↪ P.succ $x
-with P.add P.H $y ↪ P.succ $y;
-rule P.add_carry $x P.H ↪ P.add $x (P.O P.H)
-with P.add_carry P.H $y ↪ P.add (P.O P.H) $y;
-rule P.mul $x P.H ↪ $x;
+require open Stdlib.Pos;
+
+opaque symbol addnH x: π(add x H = succ x) ≔ addnH x;
+rule add $x H ↪ succ $x;
+
+opaque symbol addHn y: π(add H y = succ y) ≔ addHn y;
+rule add H $y ↪ succ $y;
+
+opaque symbol ad_carrynH x: π(add_carry x H = add x (O H)) ≔ add_carrynH x;
+rule add_carry $x H ↪ add $x (O H);
+
+opaque symbol add_carryHn y: π(add_carry H y = add (O H) y) ≔ add_carryHn y;
+rule add_carry H $y ↪ add (O H) $y;
+
+opaque symbol mul_H_right x: π(mul x H = x) ≔ mul_H_right x;
+rule mul $x H ↪ $x;
 
 // Z
 
-rule $x Z.+ Z.Z0 ↪ $x;
+require open Stdlib.Z;
+
+opaque symbol +Z0 x: π(x + Z0 = x) ≔ +Z0 x;
+rule $x + Z0 ↪ $x;
diff --git a/List.lp b/List.lp
index 8396b8d..6e4a161 100644
--- a/List.lp
+++ b/List.lp
@@ -1,7 +1,5 @@
 /* Library on polymorphic lists
 
-by Quentin Buzet (July 2022)
-
 following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v
 
 seq.v documentation
@@ -276,7 +274,7 @@ begin
     { simplify; assume y m i c; refine ⊥ₑ c }
   }
   { assume x l h; induction
-    { simplify; assume c; refine ⊥ₑ c; }
+    { simplify; assume c; refine ⊥ₑ c }
     { simplify; assume y m i c;
       apply feq2 (⸬) _ _
       { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c}
@@ -290,9 +288,9 @@ opaque symbol eql_complete a (beq : τ a → τ a → 𝔹) :
   π(`∀ x, `∀ y, x = y ⇒ beq x y) → π(`∀ l, `∀ m, l = m ⇒ eql beq l m) ≔
 begin
   assume a beq beq_complete; induction
-  { assume m i; rewrite left i; apply ⊤ᵢ; }
+  { assume m i; rewrite left i; apply ⊤ᵢ }
   { assume x l h; induction
-    { assume j; apply ⸬≠□ j; }
+    { assume j; apply ⸬≠□ j }
     { assume y m i j; simplify;
       have j': π(x = y ∧ l = m) { apply ⸬_inj j };
       apply @istrue_and (beq x y) (eql beq l m); apply ∧ᵢ
@@ -312,8 +310,8 @@ with size (_ ⸬ $l) ↪ size $l +1;
 opaque symbol size0nil [a] (l:𝕃 a) : π (size l = 0) → π (l = □) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h i; apply ⊥ₑ; apply s≠0 i; }
+  { reflexivity }
+  { assume e l h i; apply ⊥ₑ; apply s≠0 i }
 end;
 
 symbol nilp [a] l ≔ is0 (@size a l);
@@ -321,8 +319,8 @@ symbol nilp [a] l ≔ is0 (@size a l);
 opaque symbol size_behead [a] (l:𝕃 a) : π (size (behead l) = size l ∸1) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { reflexivity }
 end;
 
 // concatenation
@@ -336,19 +334,20 @@ rule □ ++ $m ↪ $m
 with ($x ⸬ $l) ++ $m ↪ $x ⸬ ($l ++ $m);
 
 opaque symbol cat0s [a] (l:𝕃 a) : π (□ ++ l = l) ≔
+begin reflexivity end;
+
+opaque symbol cats0 [a] (l:𝕃 a) : π (l ++ □ = l) ≔
 begin
-  reflexivity;
+  assume a; induction
+    { reflexivity }
+    { assume x l ih; simplify; rewrite ih; reflexivity }
 end;
 
 opaque symbol cat1s [a] (x:τ a) l : π ((x ⸬ □) ++ l = (x ⸬ l)) ≔
-begin
-  reflexivity;
-end;
+begin reflexivity end;
 
-opaque symbol cat_cons [a] (x:τ a) l1 l2 : π ((x ⸬ l1) ++ l2 = x ⸬ (l1 ++ l2)) ≔
-begin
-  reflexivity;
-end;
+opaque symbol cat_cons [a] (x:τ a) l1 l2: π ((x ⸬ l1) ++ l2 = x ⸬ (l1 ++ l2)) ≔
+begin reflexivity end;
 
 // nseq
 
@@ -367,40 +366,30 @@ with ncons ($n +1) $x $l ↪ $x ⸬ ncons $n $x $l;
 opaque symbol size_ncons [a] n (x:τ a) l : π (size (ncons n x l) = n + size l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x l; simplify; apply feq (+1) (h x l); }
+  { reflexivity }
+  { assume n h x l; simplify; apply feq (+1) (h x l) }
 end;
 
 opaque symbol size_nseq [a] n (x:τ a) : π (size (nseq n x) = n) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x; simplify; apply feq (+1) (h x); }
+  { reflexivity }
+  { assume n h x; simplify; apply feq (+1) (h x) }
 end;
 
 opaque symbol cat_nseq [a] n (x:τ a) l : π (nseq n x ++ l = ncons n x l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x l; simplify; rewrite h x l; reflexivity; }
+  { reflexivity }
+  { assume n h x l; simplify; rewrite h x l; reflexivity }
 end;
 
 opaque symbol nseqD [a] n1 n2 (x:τ a) :
   π (nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n1 h n2 x; simplify; rewrite h n2; reflexivity; }
-end;
-
-opaque symbol cats0 [a] (l:𝕃 a) : π(l ++ □ = l) ≔
-begin
-  assume a;
-  induction
-    // case l = □
-    { reflexivity; }
-    // case l = x ⸬ l'
-    { assume x l' h; simplify; rewrite h; reflexivity; }
+  { reflexivity }
+  { assume n1 h n2 x; simplify; rewrite h n2; reflexivity }
 end;
 
 opaque symbol size_cat [a] (l m : 𝕃 a) : π(size (l ++ m) = size l + size m) ≔
@@ -408,9 +397,9 @@ begin
   assume a;
   induction
     // case l = □
-    { reflexivity; }
+    { reflexivity }
     // case l = x⸬l'
-    { assume x l' h m; simplify; rewrite h; reflexivity; }
+    { assume x l' h m; simplify; rewrite h; reflexivity }
 end;
 
 opaque symbol catA  [a] (l m n : 𝕃 a) : π((l ++ m) ++ n = l ++ (m ++ n)) ≔
@@ -418,17 +407,17 @@ begin
   assume a;
   induction
     // case l = □
-    { reflexivity; }
+    { reflexivity }
     // case l = x⸬l'
-    { assume x l' h m n; simplify; rewrite h; reflexivity; }
+    { assume x l' h m n; simplify; rewrite h; reflexivity }
 end;
 
 opaque symbol cat_nilp [a] (l1 l2 : 𝕃 a) :
   π (nilp (l1 ++ l2) = (nilp l1 and nilp l2)) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h l2; simplify; reflexivity; }
+  { reflexivity }
+  { assume e l h l2; simplify; reflexivity }
 end;
 
 // list reversal
@@ -465,7 +454,7 @@ begin
     // case l = □
     { assume l; simplify; rewrite cats0; reflexivity }
     // case l = ⸬
-    { assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; rewrite catA; reflexivity; }
+    { assume x l h m; simplify ++; rewrite rev_cons; rewrite rev_cons; rewrite h; rewrite catA; reflexivity }
 end;
 
 opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
@@ -495,8 +484,8 @@ with rcons ($e ⸬ $l) $x ↪ $e ⸬ (rcons $l $x);
 opaque symbol cats1 [a] (l:𝕃 a) (z:τ a) : π (l ++ (z ⸬ □) = rcons l z) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h z; simplify; rewrite h z; reflexivity; }
+  { reflexivity }
+  { assume e l h z; simplify; rewrite h z; reflexivity }
 end;
 
 opaque symbol rcons_cons [a] (x:τ a) (s:𝕃 a) (z:τ a) :
@@ -571,8 +560,7 @@ assert ⊢ belast 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 4 ⸬ 3 ⸬ 2 ⸬ □;
 
 symbol nth [a] : τ a → 𝕃 a → ℕ → τ a;
 
-rule nth $x □ 0 ↪ $x
-with nth $x □ (_ +1) ↪ $x
+rule nth $x □ _ ↪ $x
 with nth _ ($e ⸬ _) 0 ↪ $e
 with nth $x (_ ⸬ $l) ($n +1) ↪ nth $x $l $n;
 
@@ -581,12 +569,8 @@ assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 2 ≡ 1;
 assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 3 ≡ 4;
 assert ⊢ nth 4 (3 ⸬ 2 ⸬ 1 ⸬ □) 42 ≡ 4;
 
-opaque symbol nthx□ [a: Set] n (x : τ a) : π((nth x □ n) = x)≔
-begin
-  assume n; induction
-    {reflexivity}
-    {assume m h x; reflexivity;}
-end;
+opaque symbol nthx□ [a : Set] n (x : τ a) : π((nth x □ n) = x)≔
+begin assume n; induction {reflexivity} {reflexivity} end;
 
 // set_nth
 
@@ -645,10 +629,10 @@ opaque symbol unzip1_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size la ≤ size lb) → π (unzip1 (zip la lb) = la) ≔
 begin
   assume a b; induction
-  { reflexivity; }
+  { reflexivity }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ i; }
-    { assume eb lb i j; apply feq (λ l, ea ⸬ l) (h lb j); }
+    { assume i; apply ⊥ₑ i }
+    { assume eb lb i j; apply feq (λ l, ea ⸬ l) (h lb j) }
   }
 end;
 
@@ -657,11 +641,11 @@ opaque symbol unzip2_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
 begin
   assume a b; induction
   { assume lb h;
-     have t:π (size lb = 0) { apply ≤0 (size lb) h; };
-     symmetry; apply size0nil lb t; }
+     have t:π (size lb = 0) { apply ≤0 (size lb) h };
+     symmetry; apply size0nil lb t }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i j; apply feq (λ l, eb ⸬ l) (h lb j); }
+    { reflexivity }
+    { assume eb lb i j; apply feq (λ l, eb ⸬ l) (h lb j) }
   }
 end;
 
@@ -669,10 +653,10 @@ opaque symbol size1_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size la ≤ size lb) → π (size (zip la lb) = size la) ≔
 begin
   assume a b; induction
-  { reflexivity; }
+  { reflexivity }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ i; }
-    { assume eb lb i j; apply feq (+1) (h lb j); }
+    { assume i; apply ⊥ₑ i }
+    { assume eb lb i j; apply feq (+1) (h lb j) }
   }
 end;
 
@@ -680,10 +664,10 @@ opaque symbol size2_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size lb ≤ size la) → π (size (zip la lb) = size lb) ≔
 begin
   assume a b; induction
-  { assume lb h; symmetry; apply ≤0 (size lb) h; }
+  { assume lb h; symmetry; apply ≤0 (size lb) h }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i j; apply feq (+1) (h lb j); }
+    { reflexivity }
+    { assume eb lb i j; apply feq (+1) (h lb j) }
   }
 end;
 
@@ -693,8 +677,8 @@ begin
   assume a b; induction
   { reflexivity }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i; simplify; apply feq (+1) (h lb); }
+    { reflexivity }
+    { assume eb lb i; simplify; apply feq (+1) (h lb) }
   }
 end;
 
@@ -707,14 +691,14 @@ opaque symbol seq_ind2 [a b] (p:𝕃 a → 𝕃 b → Prop) :
 begin
   assume a b p p0 pH; induction
   { induction
-    { assume h; apply p0; }
+    { assume h; apply p0 }
     { assume eb lb h1 h2; apply ⊥ₑ; apply s≠0 [size lb]; symmetry; apply h2 }
   }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ (s≠0 i); }
+    { assume i; apply ⊥ₑ (s≠0 i) }
     { assume eb lb i j;
-      have t:π (size la = size lb) { apply +1_inj j; };
-      apply pH la lb ea eb t (h lb t); }
+      have t:π (size la = size lb) { apply +1_inj j };
+      apply pH la lb ea eb t (h lb t) }
   }
 end;
 
@@ -734,13 +718,13 @@ opaque symbol nth_zip [a b] (x:τ a) (y:τ b) la lb i: π(size la = size lb) →
 begin
   assume a b x y; induction
   { assume lb i h;
-    have t: π (lb = □) { apply size0nil lb; symmetry; apply h; };
-    rewrite t; simplify; rewrite nthx□; rewrite nthx□; rewrite nthx□; reflexivity}
+    have t: π (lb = □) { apply size0nil lb; symmetry; apply h };
+    rewrite t; reflexivity}
   { assume ea la h; induction
-    { assume i j; apply ⊥ₑ (s≠0 j); }
+    { assume i j; apply ⊥ₑ (s≠0 j) }
     { assume eb lb k; induction
-      { assume m; reflexivity; }
-      { assume i m n; apply h lb i _; apply +1_inj n; }
+      { reflexivity }
+      { assume i m n; apply h lb i _; apply +1_inj n }
     }
   }
 end;
@@ -771,17 +755,10 @@ assert ⊢ drop 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 1 ⸬ 41 ⸬ □;
 assert ⊢ drop 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ □;
 
 opaque symbol dropx□ [a: Set] n: π (drop n (□ [a]) = □)≔
-begin
-  assume a;
-  induction
-    {reflexivity}
-    {reflexivity}
-  end;
+begin assume a; induction {reflexivity} {reflexivity} end;
 
 opaque symbol drop0 [a] (l:𝕃 a) : π (drop 0 l = l) ≔
-begin
-  reflexivity;
-end;
+begin reflexivity end;
 
 opaque symbol drop_oversize [a] n (l:𝕃 a) : π (size l ≤ n) → π (drop n l = □) ≔
 begin
@@ -792,21 +769,21 @@ begin
   }
   {
     assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; refine h l; }
+    { reflexivity }
+    { assume e l i; simplify; refine h l }
   }
 end;
 
 opaque symbol drop_size [a] (l:𝕃 a) : π (drop (size l) l = □) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; simplify; apply h; }
+  { reflexivity }
+  { assume e l h; simplify; apply h }
 end;
 
 opaque symbol drop_cons [a] (e:τ a) l n : π (drop (n +1) (e ⸬ l) = drop n l) ≔
 begin
-  assume a e l n; reflexivity;
+  reflexivity;
 end;
 
 opaque symbol size_drop [a] (l:𝕃 a) n : π (size (drop n l) = size l - n) ≔
@@ -814,8 +791,8 @@ begin
   assume a; induction
   { assume n; rewrite dropx□; reflexivity}
   { assume e l h; simplify; induction
-    { reflexivity; }
-    { assume n i; simplify; apply h n; }
+    { reflexivity }
+    { assume n i; simplify; apply h n }
   }
 end;
 
@@ -823,12 +800,12 @@ opaque symbol size_cons [a] (e:τ a) n l : π (size l = n ⇔ size (e ⸬ l) = n
 begin
   assume a e n l; apply ∧ᵢ {
     generalize n; induction
-    { assume l h; simplify; rewrite h; reflexivity; }
+    { assume l h; simplify; rewrite h; reflexivity }
     { assume n h l i; simplify; apply feq (+1) i;}
   } {
     generalize n; induction
     { assume l i; apply +1_inj i;}
-    { assume n h l i; apply +1_inj i; }
+    { assume n h l i; apply +1_inj i }
   };
 end;
 
@@ -837,10 +814,10 @@ opaque symbol drop_size_cat [a] n (l1 l2:𝕃 a) :
 begin
   assume a; induction
   { assume l1 l2 h; simplify;
-    have t:π (l1 = □) { apply size0nil l1 h }; rewrite t; reflexivity; }
+    have t:π (l1 = □) { apply size0nil l1 h }; rewrite t; reflexivity }
   { assume n h; induction
-    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i; }
-    { assume e l1 i l2 j; apply h l1 l2; apply +1_inj j; }
+    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i }
+    { assume e l1 i l2 j; apply h l1 l2; apply +1_inj j }
   }
 end;
 
@@ -851,8 +828,8 @@ begin
   { assume n m; rewrite dropx□; rewrite dropx□;
     rewrite dropx□; reflexivity }
   { assume e l h n1; induction
-    { simplify; rewrite addn0; reflexivity; }
-    { assume n2 i; simplify; rewrite addnS; apply h n1 n2; }
+    { simplify; rewrite addn0; reflexivity }
+    { assume n2 i; simplify; rewrite addnS; apply h n1 n2 }
   }
 end;
 
@@ -868,48 +845,39 @@ assert ⊢ take 3 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ □
 assert ⊢ take 10 (7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □) ≡ 7 ⸬ 2 ⸬ 3 ⸬ 1 ⸬ 41 ⸬ □;
 
 opaque symbol taken□ [a: Set] n: π (take n (□ [a]) = □)≔
-begin
-  assume a;
-  induction
-    {reflexivity}
-    {reflexivity}
-  end;
+begin assume a; induction {reflexivity} {reflexivity} end;
 
 opaque symbol take0 [a] (l: 𝕃 a) : π (take 0 l = □) ≔
-begin
-  reflexivity;
-end;
+begin reflexivity end;
 
 opaque symbol take_cons [a] n (x:τ a) l :
   π (take (n +1) (x ⸬ l) = (x ⸬ take n l)) ≔
-begin
-  assume a l; reflexivity;
-end;
+begin reflexivity end;
 
 opaque symbol take_size [a] (l: 𝕃 a) : π (take (size l) l = l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; simplify; rewrite h; reflexivity; }
+  { reflexivity }
+  { assume e l h; simplify; rewrite h; reflexivity }
 end;
 
 opaque symbol take_oversize [a] n (l:𝕃 a) : π (size l ≤ n) → π (take n l = l) ≔
 begin
   assume a; induction
-  { assume l h; simplify; symmetry; apply size0nil l; apply ≤0 (size l) h; }
+  { assume l h; simplify; symmetry; apply size0nil l; apply ≤0 (size l) h }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; assume j; rewrite h l j; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; assume j; rewrite h l j; reflexivity }
   }
 end;
 
 opaque symbol cat_take_drop [a] n (l:𝕃 a) : π (take n l ++ drop n l = l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity }
   }
 end;
 
@@ -917,10 +885,10 @@ opaque symbol size_takel [a] n (l:𝕃 a) :
   π (n ≤ size l) → π (size (take n l) = n) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { simplify; assume i; apply ⊥ₑ i; }
-    { assume e l i; simplify; assume j; apply feq (+1); apply h l j; }
+    { simplify; assume i; apply ⊥ₑ i }
+    { assume e l i; simplify; assume j; apply feq (+1); apply h l j }
   }
 end;
 
@@ -928,10 +896,10 @@ opaque symbol size_take_min [a] n (l:𝕃 a) :
   π (size (take n l) = min n (size l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; apply feq (+1) (h l); }
+    { reflexivity }
+    { assume e l i; simplify; apply feq (+1) (h l) }
   }
 end;
 
@@ -939,9 +907,9 @@ opaque symbol take_size_cat [a] n (l1 l2:𝕃 a) :
   π (size l1 = n) → π (take n (l1 ++ l2) = l1) ≔
 begin
   assume a; induction
-  { assume l1 l2 h; simplify; symmetry; apply size0nil l1 h; }
+  { assume l1 l2 h; simplify; symmetry; apply size0nil l1 h }
   { assume n h; induction
-    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i; }
+    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i }
     { assume e1 l1 i l2 j; simplify; apply feq (λ l, e1 ⸬ l);
       apply h l1 l2; apply ∧ₑ₂ (size_cons e1 n l1) j;
     }
@@ -952,10 +920,10 @@ opaque symbol takel_cat [a] (l1 l2:𝕃 a) n :
   π (n ≤ size l1) → π (take n (l1 ++ l2) = take n l1) ≔
 begin
   assume a; induction
-  { assume l2 n h; have t:π (n = 0) { apply ≤0 n h }; rewrite t; reflexivity; }
+  { assume l2 n h; have t:π (n = 0) { apply ≤0 n h }; rewrite t; reflexivity }
   { assume e1 l1 h l2; induction
-    { reflexivity; }
-    { assume n i j; apply feq (λ l:𝕃 a, e1 ⸬ l); apply h l2 n j; }
+    { reflexivity }
+    { assume n i j; apply feq (λ l:𝕃 a, e1 ⸬ l); apply h l2 n j }
   }
 end;
 
@@ -964,18 +932,18 @@ opaque symbol take_drop [a] m n (l:𝕃 a):
 begin
   assume a; induction
   { induction
-    { reflexivity; }
+    { reflexivity }
     { assume m h; induction
-      { reflexivity; }
+      { reflexivity }
       { assume e l i; simplify; rewrite left .[m in take m l] add0n m;
-        rewrite left h l; reflexivity; }
+        rewrite left h l; reflexivity }
     }
   }
   { assume n h; induction
     { assume l; rewrite addn0; reflexivity }
     { assume m i; induction
-      { reflexivity; }
-      { assume e l j; simplify; rewrite addnS; apply i l; }
+      { reflexivity }
+      { assume e l j; simplify; rewrite addnS; apply i l }
     }
   }
 end;
@@ -984,13 +952,13 @@ opaque symbol takeD [a] m n (l:𝕃 a) :
   π (take (m + n) l = take m l ++ take n (drop m l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume m h; induction
     { assume l; simplify; rewrite addn0; rewrite cats0; reflexivity }
     { assume n i; induction
-      { reflexivity; }
+      { reflexivity }
       { assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l); rewrite addnS;
-        rewrite left addnS; apply h (n +1) l; }
+        rewrite left addnS; apply h (n +1) l }
     }
   }
 end;
@@ -1003,8 +971,8 @@ begin
   { assume e l h; induction
     { assume i; simplify; rewrite taken□; reflexivity }
     { assume i h2; induction
-      { reflexivity; }
-      { assume j h3; simplify; rewrite h i j; reflexivity; }
+      { reflexivity }
+      { assume j h3; simplify; rewrite h i j; reflexivity }
     }
   }
 end;
@@ -1056,12 +1024,12 @@ opaque symbol take_take [a] n m :
   π (n ≤ m) → π (`∀ l:𝕃 a, take n (take m l) = take n l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { assume i; apply ⊥ₑ i; }
+    { assume i; apply ⊥ₑ i }
     { assume m i j; induction
-      { reflexivity; }
-      { assume e l k; simplify; apply feq (λ l:𝕃 a, e ⸬ l) (h m j l); }
+      { reflexivity }
+      { assume e l k; simplify; apply feq (λ l:𝕃 a, e ⸬ l) (h m j l) }
     }
   }
 end;
@@ -1080,7 +1048,7 @@ end;
 
 opaque symbol rotr0 [a] (l:𝕃 a) : π (rotr 0 l = l) ≔
 begin
-  assume a l; simplify; rewrite sub0n; rewrite take_size l; rewrite @drop_size a; reflexivity;
+  assume a l; simplify; rewrite subn0; rewrite take_size l; rewrite @drop_size a; reflexivity;
 end;
 
 // membership
@@ -1094,29 +1062,27 @@ opaque symbol in_cons [a] beq (x y:τ a) l :
   π (∈ beq x (y ⸬ l) = beq x y or ∈ beq x l) ≔
 begin
   assume a beq x y; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { reflexivity }
 end;
 
 opaque symbol in_nil [a] beq (x:τ a) : π (∈ beq x □ = false) ≔
 begin
-  assume a beq x; reflexivity;
+  reflexivity
 end;
 
 opaque symbol mem_seq1 [a] beq (x y:τ a) : π (∈ beq x (y ⸬ □) = beq x y) ≔
 begin
-  assume a beq x y;
-  simplify; rewrite or_false_lhs [beq x y];
-  reflexivity;
+  assume a beq x y; simplify; rewrite or_false; reflexivity
 end;
 
 opaque symbol mem_cat [a] beq (x:τ a) l1 l2 :
   π (∈ beq x (l1 ++ l2) = ∈ beq x l1 or ∈ beq x l2) ≔
 begin
   assume a beq x; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e1 l1 h; simplify; assume l2; rewrite h l2; rewrite orA;
-    reflexivity; }
+    reflexivity }
 end;
 
 opaque symbol mem_head [a] beq (x:τ a) l :
@@ -1222,7 +1188,7 @@ begin
     assume a  beq;
     induction
         {assume x l0; simplify ∈;
-        rewrite or_false_lhs [beq l0 x]; assume h; refine h}
+        rewrite or_false; assume h; refine h}
         {assume x l h0 l0 l1 h1 h2;
         have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
             {rewrite istrue=true h2; simplify; assume h3; refine h3 ⊤ᵢ};
@@ -1237,7 +1203,7 @@ begin
         {assume x l0 h0 h1; refine h1}
         {assume x l h0 l0 l1 h1 h2;
         have H0 : π ((¬ (istrue (beq l1 l0 or ∈ beq l1 (x ⸬ l)))) ⇒ ⊥)
-            {rewrite istrue=true h2; rewrite or_true_lhs [beq l1 l0]; simplify; assume h3; refine h3 ⊤ᵢ};
+            {rewrite istrue=true h2; rewrite or_true; simplify; assume h3; refine h3 ⊤ᵢ};
         refine H0 h1}
 end;
 
@@ -1255,7 +1221,7 @@ assert ⊢ index eqn 26 (42 ⸬ 2 ⸬ 51 ⸬ 3 ⸬ □) ≡ 4;
 opaque symbol index_size [a] beq (x:τ a) l : π (index beq x l ≤ size l) ≔
 begin
   assume a beq x; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹 (λ b, istrue (if b 0 (index beq x l +1) ≤ size l +1)) _ _ (beq x e) {
       apply ⊤ᵢ;
@@ -1304,7 +1270,7 @@ assert ⊢ find (λ x, eqn (x + 1) 3) (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ □) ≡ 4;
 opaque symbol find_size [a] (p:τ a → 𝔹) l : π (find p l ≤ size l) ≔
 begin
   assume a p; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h;
     refine ind_𝔹 (λ x, istrue (if x 0 (find p l +1) ≤ size l +1)) _ _ (p e) {
       apply ⊤ᵢ;
@@ -1327,7 +1293,7 @@ assert ⊢ count (λ x, eqn (x + 1) 3) (2 ⸬ 2 ⸬ 2 ⸬ 2 ⸬ □) ≡ 4;
 opaque symbol count_size [a] (p:τ a → 𝔹) l : π(count p l ≤ size l) ≔
 begin
   assume a p; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, istrue (if x (count p l +1) (count p l) ≤ size l +1)) _ _ (p e) {
       simplify; apply h;
@@ -1500,7 +1466,7 @@ opaque symbol size_filter [a] (p:τ a → 𝔹) l :
   π (size (filter p l) = count p l) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, size (if x (e ⸬ filter p l) (filter p l)) = (if x (count p l +1) (count p l))) _ _ (p e) {
       simplify; apply feq (+1) h;
@@ -1514,7 +1480,7 @@ opaque symbol filter_cat [a] (p:τ a → 𝔹) l1 l2 :
   π (filter p (l1 ++ l2) = filter p l1 ++ filter p l2) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e1 l1 h l2; simplify;
     refine ind_𝔹 (λ x, if x (e1 ⸬ filter p (l1 ++ l2)) (filter p (l1 ++ l2)) = if x (e1 ⸬ filter p l1) (filter p l1) ++ filter p l2) _ _ (p e1) {
       simplify; rewrite h l2; reflexivity;
@@ -1528,7 +1494,7 @@ opaque symbol filter_rev [a] (p:τ a → 𝔹) l :
   π (filter p (rev l) = rev (filter p l)) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; rewrite rev_cons; simplify filter;
     rewrite filter_cat p (rev l) (e ⸬ □); simplify filter;
     refine ind_𝔹 (λ b:𝔹, (filter p (rev l) ++ (if b (e ⸬ □) □) = rev (if b (e ⸬ filter p l) (filter p l)))) _ _ (p e) {
@@ -1553,7 +1519,7 @@ opaque symbol mem_filter [a: Set] (beq : τ a → τ a → 𝔹) (beq_correct :
 begin
     assume a beq beq_correct p;
     induction
-        {assume x h; reflexivity}
+        {reflexivity}
         {assume x0 l h0 x1 h1; simplify;
         refine ∨ₑ (case_𝔹 (p x0)) _ _
             {assume h2; rewrite h2; simplify;
@@ -1618,7 +1584,7 @@ opaque symbol filter_not_id [a] (beq : τ a → τ a → 𝔹) [l] [x]:
 begin
     assume a beq;
     induction
-        {assume x h0; reflexivity}
+        {reflexivity}
         {assume x0 l0 h0 x1 h1; simplify;
         have H0: π ((beq x1 x0) = false)
             {refine ¬istrue=false (not_mem_cons_head beq l0 x0 x1 h1)};
@@ -1700,64 +1666,64 @@ assert ⊢ map (λ x, 3 ≤ x) (42 ⸬ 2 ⸬ 51 ⸬ 3 ⸬ □) ≡ true ⸬ fals
 opaque symbol map_cons [a b] (f:τ a → τ b) l x :
   π (map f (x ⸬ l) = f x ⸬ map f l) ≔
 begin
-  assume a b f l x; reflexivity;
+  reflexivity;
 end;
 
 opaque symbol map_cat [a b] (f:τ a → τ b) l1 l2 :
   π (map f (l1 ++ l2) = map f l1 ++ map f l2) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e1 l1 h l2; simplify; rewrite h l2; reflexivity; }
+  { reflexivity }
+  { assume e1 l1 h l2; simplify; rewrite h l2; reflexivity }
 end;
 
 opaque symbol size_map [a b] (f:τ a → τ b) l : π (size (map f l) = size l) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h; simplify; apply feq (+1) h; }
+  { reflexivity }
+  { assume e l h; simplify; apply feq (+1) h }
 end;
 
 opaque symbol behead_map [a b] (f:τ a → τ b) l :
   π (behead (map f l) = map f (behead l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { reflexivity }
 end;
 
 opaque symbol map_rcons [a b] (f:τ a → τ b) l e :
   π (map f (rcons l e) = rcons (map f l) (f e)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume x l h e; simplify; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume x l h e; simplify; rewrite h e; reflexivity }
 end;
 
 opaque symbol last_map [a b] (f:τ a → τ b) l x :
   π (last (f x) (map f l) = f (last x l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h x; simplify; rewrite lastl; rewrite lastl; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume e l h x; simplify; rewrite lastl; rewrite lastl; rewrite h e; reflexivity }
 end;
 
 opaque symbol belast_map [a b] (f:τ a → τ b) l x :
   π (belast (f x) (map f l) = map f (belast x l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h x; simplify; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume e l h x; simplify; rewrite h e; reflexivity }
 end;
 
 opaque symbol map_take [a b] (f:τ a → τ b) n l :
   π (map f (take n l) = take n (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity }
   }
 end;
 
@@ -1765,10 +1731,10 @@ opaque symbol map_drop [a b] (f:τ a → τ b) n l :
   π (map f (drop n l) = drop n (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity }
   }
 end;
 
@@ -1792,9 +1758,9 @@ opaque symbol map_rev [a b] (f:τ a → τ b) l :
   π (map f (rev l) = rev (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; rewrite rev_cons; rewrite map_cat f (rev l) (e ⸬ □);
-    rewrite h; simplify map; rewrite rev_cons; reflexivity; }
+    rewrite h; simplify map; rewrite rev_cons; reflexivity }
 end;
 
 opaque symbol inj_map [a b] (f:τ a → τ b) :
@@ -1803,7 +1769,7 @@ opaque symbol inj_map [a b] (f:τ a → τ b) :
 begin
   assume a b f h; induction
   { induction
-    { reflexivity; }
+    { reflexivity }
     { simplify; assume e l i j; apply ⊥ₑ (□≠⸬ j) }
   }
   { assume e1 l1 i; induction
@@ -2013,7 +1979,7 @@ begin
   assume a;
   refine ind_𝕃2 (λ l, size ((split l)₁) + size ((split l)₂) = size l) _ _ _
   { reflexivity }
-  { assume x; reflexivity }
+  { reflexivity }
   { assume x y l ih; simplify; rewrite addnS; rewrite ih; reflexivity }
 end;
 
@@ -2057,7 +2023,7 @@ opaque symbol size_merge [a] (≤ : τ a → τ a → 𝔹) l1 l2 :
 begin
   assume a ≤;
   induction
-  { assume l2; reflexivity }
+  { reflexivity }
   { assume x l1 ih1;
     induction
     { simplify; rewrite addn0; reflexivity }
@@ -2074,7 +2040,7 @@ opaque symbol count_merge [a] p (≤ : τ a → τ a → 𝔹) l1 l2 :
 begin
   assume a p ≤;
   induction
-  { assume l2; reflexivity }
+  { reflexivity }
   { assume x l1 ih1;
     induction
     { simplify; rewrite addn0; reflexivity }
diff --git a/Nat.lp b/Nat.lp
index d41423b..db78b0e 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -1,7 +1,5 @@
 /* Library on natural numbers
 
-by Quentin Buzet (July 2022)
-
 following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v
 
 Documentation of ssrnat.v
@@ -228,9 +226,7 @@ rule _0 + $y ↪ $y
 with $x +1 + $y ↪ ($x + $y) +1;
 
 opaque symbol add0n x : π (_0 + x = x) ≔
-begin
-  assume x; reflexivity;
-end;
+begin reflexivity end;
 
 opaque symbol addn0 x : π (x + _0 = x) ≔
 begin
@@ -240,9 +236,7 @@ begin
 end;
 
 opaque symbol addSn x y : π (x +1 + y = (x + y) +1) ≔
-begin
-  assume x; reflexivity;
-end;
+begin reflexivity end;
 
 opaque symbol addnS x y : π (x + y +1 = (x + y) +1) ≔
 begin
@@ -260,7 +254,7 @@ end;
 
 opaque symbol add1n n : π ((_0 +1) + n = n +1) ≔
 begin
-  assume n; reflexivity;
+  reflexivity;
 end;
 
 opaque symbol addn1 n : π (n + (_0 +1) = n +1) ≔
@@ -438,16 +432,16 @@ rule _0 - _ ↪ _0
 with $x +1 - _0 ↪ $x +1
 with $x +1 - $y +1 ↪ $x - $y;
 
-opaque symbol sub0n n : π (n - _0 = n) ≔
+opaque symbol sub0n n : π (_0 - n = _0) ≔
 begin
-  induction
-    {reflexivity}
-    {assume n h; reflexivity}
+  reflexivity;
 end;
 
-opaque symbol subn0 n : π (_0 - n = _0) ≔
+opaque symbol subn0 n : π (n - _0 = n) ≔
 begin
-  reflexivity;
+  induction
+    {reflexivity}
+    {reflexivity}
 end;
 
 opaque symbol subnn x : π (x - x = _0) ≔
@@ -466,7 +460,7 @@ opaque symbol subn1 n : π (n - (_0 +1) = n ∸1) ≔
 begin
   induction
   { reflexivity }
-  { assume n h; simplify; rewrite sub0n; reflexivity;  }
+  { assume n h; simplify; rewrite subn0; reflexivity;  }
 end;
 
 opaque symbol subnS x y : π (x - (y +1) = (x - y) ∸1) ≔
@@ -474,7 +468,7 @@ begin
   induction
   { reflexivity }
   { assume x h; induction
-    { simplify; rewrite sub0n; reflexivity }
+    { simplify; rewrite subn0; reflexivity }
     { assume y i; simplify; rewrite h; reflexivity }
     }
 end;
@@ -491,7 +485,7 @@ begin
   induction
   { reflexivity }
   { assume x h; induction
-    { simplify; rewrite sub0n; reflexivity }
+    { simplify; rewrite subn0; reflexivity }
     { assume y i; simplify; symmetry; rewrite subnS; reflexivity }
 }
 end;
@@ -499,11 +493,11 @@ end;
 opaque symbol subnAC z x y : π ((x - y) - z = (x - z) - y) ≔
 begin
   induction
-  { assume x y; rewrite sub0n; rewrite sub0n; reflexivity }
+  { assume x y; rewrite subn0; rewrite subn0; reflexivity }
   { assume z h; induction
     { reflexivity }
     { assume x i; induction
-      { simplify; rewrite sub0n; reflexivity}
+      { simplify; rewrite subn0; reflexivity}
       { assume y j; simplify; rewrite i; rewrite subnS; symmetry;
         rewrite subnS; rewrite predn_sub; reflexivity}
     }
@@ -527,7 +521,7 @@ begin
   { assume x h; induction
     { reflexivity }
     { assume y i; induction
-      { rewrite addn0 (y +1); simplify; rewrite sub0n; reflexivity }
+      { rewrite addn0 (y +1); simplify; rewrite subn0; reflexivity }
       { assume z j; simplify; rewrite addnS y z; rewrite subnS; symmetry; rewrite subnS;
         rewrite h; reflexivity }
     }
@@ -567,14 +561,12 @@ assert x y z ⊢ x + y * z ≡ x + (y * z);
 rule _0 * _  ↪ _0
 with ($x +1) * $y ↪ $y + $x * $y;
 
-opaque symbol mul0n x : π (x * _0 = _0) ≔
-begin
-  induction { reflexivity } { assume x' h; apply h }
-end;
+opaque symbol mul0n x : π (_0 * x = _0) ≔
+begin reflexivity end;
 
-opaque symbol muln0 x : π (_0 * x = _0) ≔
+opaque symbol muln0 x : π (x * _0 = _0) ≔
 begin
-  assume x; reflexivity;
+  induction { reflexivity } { assume x' h; apply h }
 end;
 
 opaque symbol mul1n n : π ((_0 +1) * n = n) ≔
@@ -622,7 +614,7 @@ end;
 opaque symbol mulnC x y : π (x * y = y * x) ≔
 begin
   induction
-  { assume n; rewrite mul0n; reflexivity }
+  { assume n; rewrite muln0; reflexivity }
   { assume x' h y; simplify; rewrite mulnS; rewrite h; reflexivity }
 end;
 
@@ -644,9 +636,9 @@ begin
   induction
   { reflexivity }
   { assume x h; induction
-    { assume n; rewrite mul0n; simplify; rewrite mul0n; reflexivity }
+    { assume n; rewrite muln0; simplify; rewrite muln0; reflexivity }
     { assume y i; induction
-      { simplify; rewrite mul0n; rewrite sub0n; reflexivity}
+      { simplify; rewrite muln0; rewrite subn0; reflexivity}
       { assume z j; simplify; rewrite mulnS; rewrite mulnS;
         rewrite left addnAC; rewrite .[z + (x + _)] addnAC;
         rewrite subnDl; rewrite left mulSn; rewrite left mulSn;
@@ -701,7 +693,7 @@ begin
     refine ∨ₑ h _ _ {
       assume i; rewrite i; reflexivity;
     } {
-      assume i; rewrite i; rewrite mul0n; reflexivity;
+      assume i; rewrite i; rewrite muln0; reflexivity;
     };
   };
 end;
@@ -745,7 +737,7 @@ rule $x > $y ↪ $y +1 ≤ $x;
 opaque symbol ≤0 x : π (istrue (x ≤ _0)) → π (x = _0) ≔
 begin
   induction
-  { assume h; reflexivity;}
+  { reflexivity;}
   { assume x h i; apply ⊥ₑ; apply i }
 end;
 
@@ -990,7 +982,7 @@ end;
 opaque symbol leq_subr m n : π (istrue (n - m ≤ n)) ≔
 begin
   induction
-  { assume n; rewrite sub0n; apply ≤_refl n }
+  { assume n; rewrite subn0; apply ≤_refl n }
   { assume m h; induction
     { apply ⊤ᵢ }
     { assume n i; simplify;
@@ -1051,7 +1043,7 @@ opaque symbol subn_gt0 m n : π (istrue (_0 < n - m) ⇔ istrue (m < n)) ≔
 begin
   assume m n; apply ∧ᵢ {
     generalize m; induction
-    { assume n; rewrite sub0n; assume h; apply h }
+    { assume n; rewrite subn0; assume h; apply h }
     { assume m h; induction
       { assume i; apply i }
       { assume n i; rewrite subSS; assume j;
@@ -1061,7 +1053,7 @@ begin
     }
   } {
     generalize m; induction
-    { assume n h; rewrite sub0n; apply h }
+    { assume n h; rewrite subn0; apply h }
     { assume m h; induction
       { assume i; apply i }
       { assume n i j; rewrite subSS; apply h n; simplify; apply j;
@@ -1097,7 +1089,7 @@ end;
 opaque symbol subnKC m n : π (istrue (m ≤ n)) → π (m + (n - m) = n) ≔
 begin
   induction
-  { assume n h; rewrite sub0n; apply eq_refl n }
+  { assume n h; rewrite subn0; apply eq_refl n }
   { assume m h; induction
     { assume i; apply ⊥ₑ i }
     { assume n i j; apply feq (+1); apply h; apply j }
@@ -1107,9 +1099,9 @@ end;
 opaque symbol addnBn m n : π (m + (n - m) = m - n + n) ≔
 begin
   induction
-  { assume n; rewrite sub0n; apply eq_refl n }
+  { assume n; rewrite subn0; apply eq_refl n }
   { assume m h; induction
-    { rewrite subn0 (m +1); rewrite sub0n (m +1); rewrite addn0 (m +1); reflexivity }
+    { reflexivity }
     { assume n i; simplify; rewrite addnS (m - n) n; apply feq (+1); apply h n }
   }
 end;
@@ -1127,7 +1119,7 @@ begin
     rewrite t; reflexivity;
   } {
     assume n h; induction
-    { assume i; reflexivity }
+    { reflexivity }
     { assume p i j; apply h p j }
   }
 end;
@@ -1135,7 +1127,7 @@ end;
 opaque symbol addnBA m n p : π (istrue (p ≤ n))  → π (m + (n - p) = m + n - p) ≔
 begin
   induction
-  { assume n p h; reflexivity }
+  { reflexivity }
   { assume m h n p i; simplify; rewrite left addnS m (n - p);
     rewrite left addnS m n; rewrite left h (n +1) p (leqW p n i);
     rewrite subSn n p i; reflexivity;
@@ -1287,7 +1279,7 @@ end;
 opaque symbol maxnE m n : π (max m n = m + (n - m)) ≔
 begin
   induction
-  { assume n; rewrite sub0n; reflexivity }
+  { assume n; rewrite subn0; reflexivity }
   { assume m h; induction
     { simplify; rewrite addn0 m; reflexivity }
     { assume n i; simplify; rewrite h; reflexivity }
@@ -1320,7 +1312,7 @@ opaque symbol ltn_predK m n : π (istrue (m < n)) → π (n ∸1 +1 = n) ≔
 begin
   assume m; induction
   { assume h; refine ⊥ₑ h }
-  { assume n h i; reflexivity }
+  { reflexivity }
 end;
 
 opaque symbol prednK n : π (istrue (_0 < n)) → π (n ∸1 +1 = n) ≔
@@ -1362,7 +1354,7 @@ begin
     } {
       assume i;
       have t:π (n1 - n2 = _0) { apply ∧ₑ₂ (subn_eq0 n1 n2) i };
-      rewrite t; rewrite mul0n;reflexivity;
+      rewrite t; rewrite muln0;reflexivity;
     };
   }
 end;
@@ -1574,7 +1566,7 @@ end;
 opaque symbol subn_minl x y z: π ((min x y) - z = min (x - z) (y - z)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { reflexivity }
   { assume x h; induction
     { assume z; simplify; rewrite minn0; reflexivity }
     { assume y i; induction
@@ -1591,7 +1583,6 @@ begin
   { assume x h; simplify; rewrite h; reflexivity }
 end;
 
-
 opaque symbol geq_minl m n : π (istrue (min m n ≤ m)) ≔
 begin
   induction
@@ -1612,7 +1603,7 @@ end;
 opaque symbol addn_min_max m n : π (min m n + max m n = m + n) ≔
 begin
   induction
-  { assume m; reflexivity }
+  { reflexivity }
   { assume m h; induction
     { rewrite addn0 (m +1); reflexivity }
     { assume n i; simplify; rewrite addnS (min m n) (max m n);      rewrite addnS m n; rewrite h n; reflexivity }
@@ -1642,7 +1633,7 @@ end;
 opaque symbol minnK m n : π (max (min m n) m = m) ≔
 begin
   induction
-  { assume n; reflexivity }
+  { reflexivity }
   { assume m h; induction
     { reflexivity }
     { assume n i; simplify; rewrite h n; reflexivity }
@@ -1662,7 +1653,7 @@ end;
 opaque symbol maxn_minl x y z : π (max x (min y z) = min (max x y) (max x z)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { reflexivity }
   { assume x h; induction
     { assume z; simplify; rewrite minnC; rewrite maxnK (x +1) z; reflexivity }
     { assume y i; induction
@@ -1688,9 +1679,9 @@ end;
 opaque symbol minn_maxl x y z : π (min x (max y z) = max (min x y) (min x z)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { reflexivity }
     { assume y i; induction
       { reflexivity }
       { assume z j; simplify; rewrite h; reflexivity }
@@ -1703,7 +1694,7 @@ begin
   induction
   { assume y z; rewrite minn0; rewrite minn0; rewrite minn0; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { reflexivity }
     { assume y i; induction
       { reflexivity }
       { assume z j; simplify; rewrite h; reflexivity }
@@ -1714,9 +1705,9 @@ end;
 opaque symbol maxnMr x y z : π ((max y z) * x = max (y * x) (z * x)) ≔
 begin
   induction
-  { assume y z; rewrite mul0n; rewrite mul0n; rewrite mul0n;  reflexivity }
+  { assume y z; rewrite muln0; rewrite muln0; rewrite muln0;  reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { reflexivity }
     { assume y i; induction
       { reflexivity }
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
@@ -1733,11 +1724,11 @@ end;
 opaque symbol maxnMl x y z : π (x * (max y z) = max (x * y) (x * z)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { reflexivity }
   { assume x h; induction
-    { assume z; rewrite mul0n; reflexivity }
+    { assume z; rewrite muln0; reflexivity }
     { assume y i; induction
-      { rewrite mul0n; reflexivity}
+      { rewrite muln0; reflexivity}
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
         rewrite left addn_maxl (_0 +1) y z; symmetry;
         rewrite mulnDr y (_0 +1) (x +1); rewrite mulnDr z (_0 +1) (x +1);
@@ -1752,9 +1743,9 @@ end;
 opaque symbol minnMr x y z : π ((min y z) * x = min (y * x) (z * x)) ≔
 begin
   induction
-  { assume y z; rewrite mul0n; rewrite mul0n; reflexivity }
+  { assume y z; rewrite muln0; rewrite muln0; reflexivity }
   { assume x h; induction
-    { assume z; reflexivity }
+    { reflexivity }
     { assume y i; induction
       { reflexivity }
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
@@ -1771,11 +1762,11 @@ end;
 opaque symbol minnMl x y z : π (x * (min y z) = min (x * y) (x * z)) ≔
 begin
   induction
-  { assume y z; reflexivity }
+  { reflexivity }
   { assume x h; induction
-    { assume z; rewrite mul0n; simplify; rewrite mul0n; reflexivity }
+    { assume z; rewrite muln0; simplify; rewrite muln0; reflexivity }
     { assume y i; induction
-      { rewrite mul0n; simplify; rewrite mul0n; reflexivity }
+      { rewrite muln0; simplify; rewrite muln0; reflexivity }
       { assume z j; rewrite left addn1 y; rewrite left addn1 z;
         rewrite left addn_minl (_0 +1) y z; symmetry;
         rewrite mulnDr y (_0 +1) (x +1); rewrite mulnDr z (_0 +1) (x +1);
@@ -1796,19 +1787,19 @@ with $n ^ ($m +1) ↪ $n * $n ^ $m;
 
 opaque symbol expn0 m : π (m ^ _0 = _0 +1) ≔
 begin
-  assume m; reflexivity;
+  reflexivity;
 end;
 
 opaque symbol expn m : π (m ^ (_0 +1) = m) ≔
 begin
-  assume m; simplify; rewrite mulnS; rewrite mul0n m; rewrite addn0 m; reflexivity;
+  assume m; simplify; rewrite mulnS; rewrite muln0 m; rewrite addn0 m; reflexivity;
 end;
 
 opaque symbol expnS a n : π (a ^ (n +1) = a * a ^ n ) ≔
 begin
   assume a; induction
   { reflexivity }
-  { assume n h; reflexivity;}
+  { reflexivity;}
 end;
 
 opaque symbol expnSr a n : π (a ^ (n +1) = a ^ n * a) ≔
@@ -1820,7 +1811,7 @@ opaque symbol exp0n n : π (istrue (_0 < n)) → π (_0 ^ n = _0) ≔
 begin
   induction
   { assume h; refine ⊥ₑ h;}
-  { assume n h i; reflexivity }
+  { reflexivity }
 end;
 
 opaque symbol exp1n n : π ((_0 +1) ^ n = (_0 +1)) ≔
@@ -1973,7 +1964,7 @@ end;
 opaque symbol even_div2 n : π (even n) → π (div2 n + div2 n = n) ≔
 begin
   refine ind_ℕ2 (λ u, istrue (even u) ⇒ (div2 u + div2 u = u)) _ _ _
-  { assume h; reflexivity }
+  { reflexivity }
   { assume h; apply ⊥ₑ h }
   { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity }
 end;
@@ -1982,7 +1973,7 @@ opaque symbol odd_div2 n : π (odd n) → π ((div2 n + div2 n) +1 = n) ≔
 begin
   refine ind_ℕ2 (λ u, istrue (odd u) ⇒ ((div2 u + div2 u) +1 = u)) _ _ _
   { assume h; apply ⊥ₑ h }
-  { assume h; reflexivity }
+  { reflexivity }
   { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity }
 end;
 
@@ -2213,7 +2204,7 @@ opaque symbol shiftl_spec a n m : π (n ≤ m) → π (testbit (a <<< n) m = tes
 begin
 assume a;
   induction
-  { assume m h; rewrite sub0n; reflexivity }
+  { assume m h; rewrite subn0; reflexivity }
   {
     assume n ih;
     induction
diff --git a/Pos.lp b/Pos.lp
index a7b4427..0cb0165 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -1,6 +1,4 @@
-/* Positive binary integers
-
-by Quentin Garchery (May 2021). */
+// Positive binary integers following Rocq stdlib
 
 require open Stdlib.Nat Stdlib.Comp;
 
@@ -106,7 +104,7 @@ opaque opaque symbol valS x : π(val (succ x) = val x +1) ≔
 begin
   induction
   { assume x h; simplify; rewrite h; simplify; rewrite addn0; rewrite addnS; reflexivity}
-  { assume x h; reflexivity }
+  { reflexivity }
   { reflexivity }
 end;
 
@@ -255,7 +253,7 @@ with add_carry H      (I $q) ↪ I (succ $q)
 with add_carry H      (O $q) ↪ O (succ $q)
 with add_carry H      H      ↪ I H;
 
-opaque symbol add_carryH n : π (add_carry n H = add n (O H))≔
+opaque symbol add_carrynH n : π (add_carry n H = add n (O H))≔
 begin
   induction
     {assume n h; simplify; rewrite addnH; reflexivity }
@@ -599,7 +597,7 @@ begin
   { assume x xrec;
     induction
      { assume y h c; simplify; refine compare_Gt_succ x y }
-     { assume y h c; reflexivity }
+     { reflexivity }
      { assume c; simplify; refine compare_Gt_H x } }
   // case H
   { induction
diff --git a/Z.lp b/Z.lp
index 84187e1..4550574 100644
--- a/Z.lp
+++ b/Z.lp
@@ -1,6 +1,4 @@
-/* Binary integers
-
-by Quentin Garchery (May 2021). */
+// Binary integers (following Rocq stdlib)
 
 require open Stdlib.Pos;
 
@@ -536,7 +534,7 @@ end;
 opaque symbol *_distr_l (z x y : ℤ) : π (z * (x + y) = z * x + z * y) ≔
 begin
   induction
-  { assume x y; reflexivity }
+  { reflexivity }
   { assume z;
     induction
     { reflexivity }
@@ -552,7 +550,7 @@ begin
       { assume y; simplify; rewrite mul_distr_l; reflexivity } } }
   { assume z;
     induction
-    { assume x; reflexivity }
+    { reflexivity }
     { assume x;
       induction
       { reflexivity }
@@ -783,9 +781,9 @@ end;
 opaque symbol ≐_mul_Zpos w r : π ((w * Zpos r ≐ Z0) = (w ≐ Z0)) ≔
 begin
   induction
-   { assume r; reflexivity }
-   { assume a r; reflexivity }
-   { assume a r; reflexivity }
+   { reflexivity }
+   { reflexivity }
+   { reflexivity }
 end;
 
 // ℤ has no zero divisor