diff --git a/paper/proof_irr.lp b/paper/proof_irr.lp
index c4ddbf6b9279f9abe35ee25b37d5058638c5ff19..31933a840655baa6d36b37e392da7cfa07456151 100644
--- a/paper/proof_irr.lp
+++ b/paper/proof_irr.lp
@@ -15,10 +15,10 @@ symbol p1: Prf (z ≤ s z)
 symbol p2: Prf (z ≤ s z)
 definition bounded (k: El ℕ) ≔ psub (λn, n ≤ k)
 
-constant symbol slist (bound: El â„•): Set
+constant symbol slist (_: El â„•): Set
 constant symbol snil (bound: El â„•): El (slist bound)
 constant symbol scons {bound: El â„•} (head: El (bounded bound))
-                      (tail: El (slist (fst head)))
+                      (_: El (slist (fst head)))
               : El (slist bound)
 
 set declared "l₁"
@@ -40,7 +40,7 @@ symbol app_pair {a b: Set} (x y: El a) (p: El a → Bool)
 symbol plus: El ℕ → El ℕ → El ℕ
 set infix left 10 "+" ≔ plus
 
-constant symbol even_p: El ℕ → Bool
+symbol even_p: El ℕ → Bool
 definition even ≔ psub even_p
 
 symbol plus_closed_even (n m: El even): Prf (even_p ((fst n) + (fst m)))
@@ -48,12 +48,6 @@ symbol plus_closed_even (n m: El even): Prf (even_p ((fst n) + (fst m)))
 definition add (n m: El even) : El even
          ≔ pair ((fst n) + (fst m)) (plus_closed_even n m)
 
-symbol app_thm (a b: Set) (f: El (a ~> b))
-               (x y: El a) (_: Prf (x = y))
-     : Prf (f x = f y)
-
-symbol fun_ext (a b: Set) (f g: El (a ~> b)) (_: Prf (∀ (λx, f x = g x))): Prf (f = g)
-
 symbol plus_commutativity (n m: El â„•): Prf (n + m = m + n)
 
 theorem even_add_commutativity (n m: El even): Prf (add n m = add m n)
@@ -68,19 +62,3 @@ proof
   // fst n + m = fst m + n
   refine plus_commutativity (fst n) (fst m)
 qed
-
-// Toy example
-set declared "nâ‚€"
-set declared "n₁"
-symbol nâ‚€: El â„•
-symbol n₁: El ℕ
-
-symbol nz_eq_no: Prf (n₀ = n₁)
-symbol pred: El ℕ → Bool
-symbol pq0: Prf (pred nâ‚€)
-symbol pq1: Prf (pred n₁)
-
-definition ps ≔ psub pred
-theorem thethm: Prf (@pair ℕ pred n₀ pq0 = @pair ℕ pred n₁ pq1)
-proof
-admit