diff --git a/README.org b/README.org
index 9dc6d7d..afe59f6 100644
--- a/README.org
+++ b/README.org
@@ -200,6 +200,9 @@ Right now, if there's a failure, everything just stops immediately. More increme
 *** TODO Multiple levels of AST
 Right now, the parsing and typechecking kind of happens all at once on a single syntax representation. As I add fancier and fancier elaboration, it might be a good idea to have multiple syntax representations. So we'd have one level of syntax representing what is actually in the file (modulo some easy elaboration like with function definitions), and through a series of transformations transform it into something like the current =Expr= type with all the information needed for typechecking and all the complex language features removed.
 
+*** TODO Improve type checking algorithm
+I'm proud that I just kinda made up a working type checking algorithm, but it is clearly quite flawed. Even assuming no need to check beta equivalence, I'm pretty sure that this algorithm is approximately exponential in the length of a term, which is pretty terrible. It hasn't been a huge problem, but type checking just the term =R2_sub_R= in <examples/peano.pg> takes about 1.5 seconds. Performance could easily be drastically improved with some memoization, but upgrading to an off-the-shelf bidirectional type checking algorithm seems like a good idea in general. Another problem with my current type checking algorithm is that it is very inflexible (e.g. adding optional return type ascriptions in functions, or type ascriptions in =let= bindings is currently impossible, while trivial to add with bidirectional type checking). I also have no idea how to add [[Inference][type inference]] or [[Implicits][implicits]] with how things are currently structured. A more flexible type checking algorithm, likely together with [[Multiple levels of AST][multiple levels of AST]], makes it seem more possible.
+
 *** TODO Alternate syntax
 I've had a bunch of ideas for a more mathematician-friendly syntax bouncing around my head for a while. Implementing one of them would be awesome, but probably quite tricky.
 
diff --git a/examples/logic.pg b/examples/logic.pg
index bb15f35..261bc21 100644
--- a/examples/logic.pg
+++ b/examples/logic.pg
@@ -161,11 +161,13 @@ and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
 
 -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
 and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
-    and_intro A (and B C)
-        (and_elim_l A B (and_elim_l (and A B) C h))
-        (and_intro B C
-            (and_elim_r A B (and_elim_l (and A B) C h))
-            (and_elim_r (and A B) C h));
+    let (ab := and_elim_l (and A B) C h)
+        (a := and_elim_l A B ab)
+        (b := and_elim_r A B ab)
+        (c := and_elim_r (and A B) C h)
+    in
+        and_intro A (and B C) a (and_intro B C b c)
+    end;
 
 -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
 or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
diff --git a/examples/peano.pg b/examples/peano.pg
index 53d9b66..9f95907 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -1,7 +1,6 @@
--- 
--- We need some basic logic, so I'm stealing this from <logic.pg>. See that file
--- for more details on how these work.
--- 
+-- {{{ Logic/general definitions
+
+-- import basic logic definitions from <logic.pg>
 
 @include logic.pg
 
@@ -13,9 +12,10 @@ comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
 assoc (A : *) (op : binop A) := forall (c a b : A),
   eq A (op a (op b c)) (op (op a b) c);
 
--- --------------------------------------------------------------------------------------------------------------
+-- }}}
+
+-- {{{ Axioms
 
--- 
 -- Now we can define the Peano axioms. Unlike with equality, perga is not
 -- powerful enough to construct the natural numbers (or at least to prove the
 -- Peano axioms as theorems from a definition constructible in perga). However,
@@ -27,11 +27,9 @@ assoc (A : *) (op : binop A) := forall (c a b : A),
 -- trust our type ascription, and assume going forward that the identifier we
 -- defined is a value of the asserted type. For example, we will use the axiom
 -- system to assert the existence of a type of natural numbers
--- 
 
 nat : * := axiom;
 
--- 
 -- As you can imagine, this can be risky. For instance, there's nothing stopping
 -- us from saying
 --     uh_oh : false := axiom;
@@ -51,7 +49,6 @@ nat : * := axiom;
 -- so we should be fine. I'm formalizing the second order axioms given in the
 -- wikipedia article on the Peano axioms
 -- (https://en.wikipedia.org/wiki/Peano_axioms).
--- 
 
 -- axiom 1: 0 is a natural number
 zero : nat := axiom;
@@ -65,14 +62,15 @@ suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m := axiom;
 -- axiom 8: No successor of any natural number is zero.
 suc_nonzero : forall (n : nat), not (eq nat (suc n) zero) := axiom;
 
--- axiom 9: Induction! For any proposition φ on natural numbers, if φ(0) holds,
--- and if for every natural number n, φ(n) ⇒ φ(S n), then φ holds for all n.
-nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc n))
-    -> forall (n : nat), φ n := axiom;
+-- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
+-- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
+nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
+    -> forall (n : nat), P n := axiom;
 
--- --------------------------------------------------------------------------------------------------------------
+-- }}}
+
+-- {{{ Basic Definitions
 
--- 
 -- Now that we have stipulated these axioms, we are free to use them to make
 -- definitions, prove theorems, etc.
 -- 
@@ -81,7 +79,6 @@ nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc
 -- 
 -- First, we will make a bunch of abbreviations, since these terms get really
 -- long and complicated really quickly.
--- 
 
 -- Some abbreviations for common numbers.
 one   : nat := suc zero;
@@ -117,224 +114,486 @@ suc_or_zero : forall (n : nat), szc n :=
             or_intro_r (szc_l (suc n)) (szc_r (suc n))
                 (exists_intro nat (pred (suc n)) n (eq_refl nat (suc n))));
 
--- 
--- Before we continue one to defining addition, we need one more bunch of
--- axioms. Addition is normally defined recursively, which is difficult without
--- inductive definitions. I'm pretty sure this axiom is derivable from the
--- others, but I've spent a very long time trying to derive it, and it has
--- proven extremely difficult. I'm still convinced it's possible, just
--- prohibitively difficult and tedious without further language features
--- (implicit arguments and let bindings would help a ton).
--- 
--- Normally, we define recursive functions f : nat -> A in the following format:
---            f 0 = fzero
---      f (suc n) = fsuc n (f n)
--- More concretely, we have two equations, one for each possible case for n,
--- i.e. either zero or a successor. In the successor case, the value of
--- f (suc n) can depend on the value of f n. The recursion axioms below
--- assert that for any such pair of equations, there exists a unique function
--- satisfying said equations.
--- 
+-- }}}
 
--- For any such equations, there exists a function.
-rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
+-- {{{ Recursive Definitions
 
--- Here's equation one.
-rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := 
-  eq A (f zero) fzero;
+-- The next step would normally be to define addition and prove properties of
+-- addition. However, we need to take a very long and difficult detour in order
+-- to be able to define addition in the first place. The normal way addition is
+-- defined is by the following two equations:
+--
+-- 1)       n + 0 = n
+-- 2) n + (suc m) = suc (n + m)
+--
+-- It is clear that this definition is ok, since m gets smaller with every
+-- application of equation 2, until m reaches zero, whereupon we can use
+-- equation 1. This argument, while perfectly reasonable, is deceptively
+-- difficult to formalize. It turns out that this structure of recursively
+-- defining a function by two equations similar to 1 and 2 is extremely common.
+-- So, we will take the time to prove the following theorem.
+--
+-- Theorem (recursive definitions):
+-- For every type A, element z : A, and function fS : nat -> A -> A, there
+-- exists a unique function f : nat -> A satisfying
+-- 1)                       f 0 = z
+-- 2) forall n : nat, f (suc n) = fS n (f n)
+--
+-- Once we've proved this theorem, we can easily define addition such that,
+-- i.e. that for any fixed n : nat, "n+" is the unique function satisfying
+-- 1)                       n + 0 = n
+-- 2) forall m : nat, n + (suc m) = suc (n + m)
+-- Notice that this is the exact form we need in order to apply the theorem.
+--
+-- However, proving this theorem is *extremely long and difficult*. I would
+-- recommend skipping this section and coming back to it after you are much
+-- more used to perga. As such, I will go into a lot less detail on each of
+-- these proofs than in the later sections.
+--
+-- Here's our game plan. We will define a relation R : nat -> A -> * such that
+-- R x y iff for every relation Q : nat -> A -> * satisfying
+-- 1) Q 0 z and
+-- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
+-- Q x y.
+-- In more math lingo, we take R to be the intersection of every relation
+-- satisfying 1 and 2. From there we will, with much effort, prove that R is
+-- actually a function satisfying the equations we want it to.
 
--- And equation two.
-rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
-  forall (n : nat) (y : A),
-    eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
+-- {{{ Defining R
+-- Here is condition 1 formally expressed in perga.
+cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+    Q zero z;
 
--- Said function satisfies the equations.
--- It satisfies equation one.
-rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
-  rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
+-- Likewise for condition 2.
+cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+    forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
 
--- And two.
-rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
-  rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
+-- From here we can define R.
+rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+    forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
+-- }}}
 
--- And, finally, this function is unique in the sense that if any other function
--- also satisfies the equations, it takes the same values as rec_def.
-rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
-  rec_cond_zero A fzero fsuc f ->
-  rec_cond_suc  A fzero fsuc f ->
-  rec_cond_zero A fzero fsuc g ->
-  rec_cond_suc  A fzero fsuc g ->
-  forall (x : nat), eq A (f x) (g x) := axiom;
+-- {{{ R is total
+total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
 
--- Now we can safely define addition.
+rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
+    fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;
 
--- First, here's the RHS of equation 2 as a function, since it will show up
--- multiple times.
-psuc (_ r : nat) := suc r;
+rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
+    fun (n : nat) (y : A) (h : rec_rel A z fS n y)
+        (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
+        h2 n y (h Q h1 h2);
 
--- And here's plus!
-plus (n : nat) : nat -> nat := rec_def nat n psuc;
+rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
+    let (R := rec_rel A z fS)
+        (P (x : nat) := exists A (R x))
+        (c1 := cond1 A z fS)
+        (c2 := cond2 A z fS)
+    in
+    nat_ind P
+    (exists_intro A (R zero) z (rec_rel_cond1 A z fS))
+    (fun (n : nat) (IH : P n) =>
+        exists_elim A (P (suc n)) (R n) IH
+        (fun (y0 : A) (hy : R n y0) =>
+            exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 A z fS n y0 hy)))
+    end;
+-- }}}
 
--- The first equation manifests itself as the familiar
---      n + 0 = 0.
-plus_0_r (n : nat) : eq nat (plus n zero) n :=
-  rec_def_sat_zero nat n psuc;
+-- {{{ Defining R2
+alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
+    and (eq nat x zero) (eq A y z);
 
--- The second equation, after a bit of massaging, manifests itself as the
--- likewise familiar
---      n + suc m = suc (n + m).
-plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
-  rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m));
+cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
+    (x2 : nat) (y2 : A) :=
+        and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);
 
--- We can now prove 1 + 1 = 2!
-one_plus_one_two : eq nat (plus one one) two :=
-  -- 1 + (suc zero) = suc (1 + zero) = suc one
-  eq_trans nat (plus one one) (suc (plus one zero)) two
+cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
+    and (pred x x2) (exists A (cond_y2 A z fS x y x2));
 
-  -- 1 + (suc zero) = suc (1 + zero)
-  (plus_s_r one zero)
+alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+    exists nat (cond_x2 A z fS x y);
 
-  -- suc (1 + zero) = suc one
-  (eq_cong nat nat (plus one zero) one suc (plus_0_r one));
+rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+    or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
+-- }}}
 
--- 
--- We have successfully defined addition! Note that evaluating 1 + 1 to 2
--- requires a proof, unfortunately, since this computation isn't visible to
--- perga.
--- 
--- We will now prove a couple standard properties of addition.
--- 
+-- {{{ R = R2
 
--- First, associativity, namely that n + (m + p) = (n + m) + p.
-plus_assoc : assoc nat plus := 
-  -- We prove this via induction on p.
-  nat_ind
-    (fun (p : nat) =>
-      forall (n m : nat),
-        eq nat (plus n (plus m p)) (plus (plus n m) p))
+-- {{{ R2 ⊆ R
+R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+    rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
+    let (R := rec_rel A z fS)
+        (R2 := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 A z x y)
+        (ac2 := alt_cond2 A z fS x y)
+    in
+        fun (h : R2 x y) =>
+            or_elim ac1 ac2 (R x y) h
+            (fun (case1 : ac1) =>
+                let
+                    (x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
+                    (yz := and_elim_r (eq nat x zero) (eq A y z) case1)
+                    (a1 := (eq_sym A y z yz) (R zero) (rec_rel_cond1 A z fS))
+                in
+                    (eq_sym nat x zero x0) (fun (n : nat) => R n y) a1
+                end)
+            (fun (case2 : ac2) =>
+                let (h1 := cond_x2 A z fS x y)
+                    (h2 := cond_y2 A z fS x y)
+                in
+                exists_elim nat (R x y) h1 case2
+                (fun (x2 : nat) (hx2 : h1 x2) =>
+                    let (hpred := and_elim_l (pred x x2) (exists A (h2 x2)) hx2)
+                        (hex := and_elim_r (pred x x2) (exists A (h2 x2)) hx2)
+                    in
+                    exists_elim A (R x y) (h2 x2) hex
+                    (fun (y2 : A) (hy2 : h2 x2 y2) =>
+                        let (hpreim := and_elim_l (eq A y (fS x2 y2)) (R x2 y2) hy2)
+                            (hR := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2)
+                            (a1 := rec_rel_cond2 A z fS x2 y2 hR)
+                            (a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1)
+                        in
+                            (eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2
+                        end)
+                    end)
+                end)
+    end;
+-- }}}
 
-    -- Base case: p = 0
-    -- WTS n + (m + 0) = (n + m) + 0
-    (fun (n m : nat) =>
-      -- n + (m + 0) = n + m = (n + m) + 0
-      (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
-        -- n + (m + 0) = n + m
-        (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
+-- {{{ R ⊆ R2
+R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
+    or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
+    (and_intro (eq nat zero zero) (eq A z z)
+        (eq_refl nat zero)
+        (eq_refl A z));
 
-        -- n + m = (n + m) + 0
-        (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m)))))
+R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
+    let (R := rec_rel A z fS)
+        (R2 := rec_rel_alt A z fS)
+    in
+        fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
+        let (x := suc x2)
+            (y := fS x2 y2)
+            (cx2 := cond_x2 A z fS x y)
+            (cy2 := cond_y2 A z fS x y x2)
+        in
+            or_intro_r (alt_cond1 A z x y) (alt_cond2 A z fS x y)
+            (exists_intro nat cx2 x2
+                (and_intro (pred x x2) (exists A cy2)
+                    (eq_refl nat x)
+                    (exists_intro A cy2 y2
+                        (and_intro (eq A y y) (R x2 y2)
+                            (eq_refl A y)
+                            (R2_sub_R A z fS x2 y2 h)))))
+        end
+    end;
 
-    -- Inductive step: IH = n + (m + p) = (n + m) + p
-    (fun (p : nat) (IH : forall (n m : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)) (n m : nat) =>
-      -- WTS n + (m + suc p) = (n + m) + suc p
-      -- n + (m + suc p) = n + suc (m + p)
-      --                 = suc (n + (m + p))
-      --                 = suc ((n + m) + p)
-      --                 = (n + m) + suc p
-      eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
+R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+    rec_rel A z fS x y -> rec_rel_alt A z fS x y :=
+    let (R := rec_rel A z fS)
+        (R2 := rec_rel_alt A z fS)
+    in
+        fun (h : R x y) =>
+            h R2 (R2_cond1 A z fS) (R2_cond2 A z fS)
+    end;
+-- }}}
 
-      -- n + (m + suc p) = n + suc (m + p)
-      (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
+-- }}}
 
-      -- n + suc (m + p) = (n + m) + suc p
-      (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
-        -- n + suc (m + p) = suc (n + (m + p))
-        (plus_s_r n (plus m p))
+-- {{{ R2 (hence R) is functional
 
-        -- suc (n + (m + p)) = (n + m) + suc p
-        (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
-          -- suc (n + (m + p)) = suc ((n + m) + p)
-          (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc (IH n m))
+fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
+    R x y1 -> R x y2 -> eq B y1 y2;
 
-          -- suc ((n + m) + p) = (n + m) + suc p
-          (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
-            (plus_s_r (plus n m) p)))));
+fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
 
--- Up next is commutativity, but we will need a couple lemmas first.
+R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
+    rec_rel_alt A z fS zero y -> eq A y z :=
+    let (R2 := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 A z zero y)
+        (ac2 := alt_cond2 A z fS zero y)
+        (cx2 := cond_x2 A z fS zero y)
+        (cy2 := cond_y2 A z fS zero y)
+    in fun (h : R2 zero y) =>
+        or_elim ac1 ac2 (eq A y z) h
+        (fun (case1 : ac1) => and_elim_r (eq nat zero zero) (eq A y z) case1)
+        (fun (case2 : ac2) =>
+            exists_elim nat (eq A y z) cx2 case2
+            (fun (x2 : nat) (h2 : cx2 x2) =>
+                suc_nonzero x2
+                (eq_sym nat zero (suc x2) (and_elim_l (pred zero x2) (exists A (cy2 x2)) h2))
+                (eq A y z)))
+    end;
 
--- First, we will show that 0 + n = n.
-plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
-  -- We prove this by induction on n.
-  nat_ind (fun (n : nat) => eq nat (plus zero n) n)
-    -- base case: WTS 0 + 0 = 0
-    -- This is just plus_0_r 0
-    (plus_0_r zero)
+R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
+    rec_rel_alt A z fS (suc x2) y -> exists A (cond_y2 A z fS (suc x2) y x2) :=
+    let (R2 := rec_rel_alt A z fS)
+        (x := suc x2)
+        (ac1 := alt_cond1 A z x y)
+        (ac2 := alt_cond2 A z fS x y)
+        (cx2 := cond_x2 A z fS x y)
+        (cy2 := cond_y2 A z fS x y)
+        (goal := exists A (cy2 x2))
+    in
+        fun (h : R2 x y) =>
+        or_elim ac1 ac2 goal h
+        (fun (case1 : ac1) => suc_nonzero x2 (and_elim_l (eq nat x zero) (eq A y z) case1) goal)
+        (fun (case2 : ac2) =>
+            exists_elim nat goal cx2 case2
+            (fun (x22 : nat) (hx22 : cx2 x22) =>
+                let (hpred := and_elim_l (pred x x22) (exists A (cy2 x22)) hx22)
+                    (hgoal := and_elim_r (pred x x22) (exists A (cy2 x22)) hx22)
+                    (x2_x22 := suc_inj x2 x22 hpred)
+                in
+                    (eq_sym nat x2 x22 x2_x22)
+                    (fun (n : nat) => exists A (cy2 n))
+                    hgoal
+                end))
+    end;
 
-    -- inductive case
-    (fun (n : nat) (IH : eq nat (plus zero n) n) =>
-      -- WTS 0 + (suc n) = suc n
-      -- 0 + (suc n) = suc (0 + n) = suc n
-      eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
-      -- 0 + (suc n) = suc (0 + n)
-      (plus_s_r zero n)
+R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
+    let (R := rec_rel A z fS)
+        (R2 := rec_rel_alt A z fS)
+        (f_in := fl_in nat A R2)
+    in nat_ind f_in
+        (fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) =>
+            eq_trans A y1 z y2
+            (R2_zero A z fS y1 h1)
+            (eq_sym A y2 z (R2_zero A z fS y2 h2)))
+        (fun (x2 : nat) (IH : f_in x2) (y1 y2 : A) (h1 : R2 (suc x2) y1) (h2 : R2 (suc x2) y2) =>
+            let (x := suc x2)
+                (cy1 := cond_y2 A z fS x y1 x2)
+                (cy2 := cond_y2 A z fS x y2 x2)
+                (goal := eq A y1 y2)
+            in
+                exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1)
+                (fun (y12 : A) (h12 : cy1 y12) =>
+                    exists_elim A goal cy2 (R2_suc A z fS x2 y2 h2)
+                    (fun (y22 : A) (h22 : cy2 y22) =>
+                        let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (R x2 y12) h12)
+                            (y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (R x2 y22) h22)
+                            (R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (R x2 y12) h12)
+                            (R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (R x2 y22) h22)
+                            (R2_x2_y12 := R_sub_R2 A z fS x2 y12 R_x2_y12)
+                            (R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22)
+                            (y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22)
+                        in
+                            eq_trans A y1 (fS x2 y12) y2
+                            y1_preim
+                            (eq_trans A (fS x2 y12) (fS x2 y22) y2
+                                (eq_cong A A y12 y22 (fun (y : A) => fS x2 y) y12_y22)
+                                (eq_sym A y2 (fS x2 y22) y2_preim))
+                        end))
+            end)
+    end;
 
-      -- suc (0 + n) = suc n
-      (eq_cong nat nat (plus zero n) n suc IH));
+-- }}}
 
--- Next, we will show that (suc n) + m = suc (n + m).
-plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
-  -- We proceed by induction on m.
-  nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
-    -- base case: (suc n) + 0 = suc (n + 0)
-    -- (suc n) + 0 = suc n = suc (n + 0)
-    (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
-      -- (suc n) + 0 = suc n
-      (plus_0_r (suc n))
+rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
+    exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
+        (fun (y : A) (_ : rec_rel A z fS x y) => y);
 
-      -- suc n = suc (n + 0)
-      (eq_cong nat nat n (plus n zero) suc
-        -- n = n + 0
-        (eq_sym nat (plus n zero) n (plus_0_r n))))
+-- }}}
 
-    -- inductive case
-    -- IH = suc n + m = suc (n + m)
-    (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) =>
-        -- WTS suc n + suc m = suc (n + suc m)
-        -- suc n + suc m = suc (suc n + m)
-        --               = suc (suc (n + m))
-        --               = suc (n + suc m)
-        (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m)))
-          -- suc n + suc m = suc (suc n + m)
-          (plus_s_r (suc n) m)
-
-          -- suc (suc n + m) = suc (n + suc m)
-          (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
-            -- suc (suc n + m) = suc (suc (n + m))
-            (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
-
-            -- suc (suc (n + m)) = suc (n + suc m)
-            (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
-              -- suc (n + m) = n + suc m
-              (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
-
--- Finally, we can prove commutativity.
-plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
-  -- As usual, we proceed by induction.
-  nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
-
-  -- Base case: WTS n + 0 = 0 + n
-  -- n + 0 = n = 0 + n
-  (eq_trans nat (plus n zero) n (plus zero n)
-    -- n + 0 = n
-    (plus_0_r n)
-
-    -- n = 0 + n
-    (eq_sym nat (plus zero n) n (plus_0_l n)))
-
-  -- Inductive step:
-  (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
-    -- WTS n + suc m = suc m + n
-    -- n + suc m = suc (n + m)
-    --           = suc (m + n)
-    --           = suc m + n
-    (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
-      -- n + suc m = suc (n + m)
-      (plus_s_r n m)
-
-      -- suc (n + m) = suc m + n
-      (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
-        -- suc (n + m) = suc (m + n)
-        (eq_cong nat nat (plus n m) (plus m n) suc IH)
-
-        -- suc (m + n) = suc m + n
-        (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));
+-- -- For any such equations, there exists a function.
+-- rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
+--
+-- -- Here's equation one.
+-- rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := 
+--   eq A (f zero) fzero;
+--
+-- -- And equation two.
+-- rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
+--   forall (n : nat) (y : A),
+--     eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
+--
+-- -- Said function satisfies the equations.
+-- -- It satisfies equation one.
+-- rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
+--   rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
+--
+-- -- And two.
+-- rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
+--   rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
+--
+-- -- And, finally, this function is unique in the sense that if any other function
+-- -- also satisfies the equations, it takes the same values as rec_def.
+-- rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
+--   rec_cond_zero A fzero fsuc f ->
+--   rec_cond_suc  A fzero fsuc f ->
+--   rec_cond_zero A fzero fsuc g ->
+--   rec_cond_suc  A fzero fsuc g ->
+--   forall (x : nat), eq A (f x) (g x) := axiom;
+--
+-- -- Now we can safely define addition.
+--
+-- -- First, here's the RHS of equation 2 as a function, since it will show up
+-- -- multiple times.
+-- psuc (_ r : nat) := suc r;
+--
+-- -- And here's plus!
+-- plus (n : nat) : nat -> nat := rec_def nat n psuc;
+--
+-- -- The first equation manifests itself as the familiar
+-- --      n + 0 = 0.
+-- plus_0_r (n : nat) : eq nat (plus n zero) n :=
+--   rec_def_sat_zero nat n psuc;
+--
+-- -- The second equation, after a bit of massaging, manifests itself as the
+-- -- likewise familiar
+-- --      n + suc m = suc (n + m).
+-- plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
+--   rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m));
+--
+-- -- We can now prove 1 + 1 = 2!
+-- one_plus_one_two : eq nat (plus one one) two :=
+--   -- 1 + (suc zero) = suc (1 + zero) = suc one
+--   eq_trans nat (plus one one) (suc (plus one zero)) two
+--
+--   -- 1 + (suc zero) = suc (1 + zero)
+--   (plus_s_r one zero)
+--
+--   -- suc (1 + zero) = suc one
+--   (eq_cong nat nat (plus one zero) one suc (plus_0_r one));
+--
+-- -- 
+-- -- We have successfully defined addition! Note that evaluating 1 + 1 to 2
+-- -- requires a proof, unfortunately, since this computation isn't visible to
+-- -- perga.
+-- -- 
+-- -- We will now prove a couple standard properties of addition.
+-- -- 
+--
+-- -- First, associativity, namely that n + (m + p) = (n + m) + p.
+-- plus_assoc : assoc nat plus := 
+--   -- We prove this via induction on p.
+--   nat_ind
+--     (fun (p : nat) =>
+--       forall (n m : nat),
+--         eq nat (plus n (plus m p)) (plus (plus n m) p))
+--
+--     -- Base case: p = 0
+--     -- WTS n + (m + 0) = (n + m) + 0
+--     (fun (n m : nat) =>
+--       -- n + (m + 0) = n + m = (n + m) + 0
+--       (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
+--         -- n + (m + 0) = n + m
+--         (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
+--
+--         -- n + m = (n + m) + 0
+--         (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m)))))
+--
+--     -- Inductive step: IH = n + (m + p) = (n + m) + p
+--     (fun (p : nat) (IH : forall (n m : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)) (n m : nat) =>
+--       -- WTS n + (m + suc p) = (n + m) + suc p
+--       -- n + (m + suc p) = n + suc (m + p)
+--       --                 = suc (n + (m + p))
+--       --                 = suc ((n + m) + p)
+--       --                 = (n + m) + suc p
+--       eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
+--
+--       -- n + (m + suc p) = n + suc (m + p)
+--       (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
+--
+--       -- n + suc (m + p) = (n + m) + suc p
+--       (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
+--         -- n + suc (m + p) = suc (n + (m + p))
+--         (plus_s_r n (plus m p))
+--
+--         -- suc (n + (m + p)) = (n + m) + suc p
+--         (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
+--           -- suc (n + (m + p)) = suc ((n + m) + p)
+--           (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc (IH n m))
+--
+--           -- suc ((n + m) + p) = (n + m) + suc p
+--           (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
+--             (plus_s_r (plus n m) p)))));
+--
+-- -- Up next is commutativity, but we will need a couple lemmas first.
+--
+-- -- First, we will show that 0 + n = n.
+-- plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
+--   -- We prove this by induction on n.
+--   nat_ind (fun (n : nat) => eq nat (plus zero n) n)
+--     -- base case: WTS 0 + 0 = 0
+--     -- This is just plus_0_r 0
+--     (plus_0_r zero)
+--
+--     -- inductive case
+--     (fun (n : nat) (IH : eq nat (plus zero n) n) =>
+--       -- WTS 0 + (suc n) = suc n
+--       -- 0 + (suc n) = suc (0 + n) = suc n
+--       eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
+--       -- 0 + (suc n) = suc (0 + n)
+--       (plus_s_r zero n)
+--
+--       -- suc (0 + n) = suc n
+--       (eq_cong nat nat (plus zero n) n suc IH));
+--
+-- -- Next, we will show that (suc n) + m = suc (n + m).
+-- plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
+--   -- We proceed by induction on m.
+--   nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
+--     -- base case: (suc n) + 0 = suc (n + 0)
+--     -- (suc n) + 0 = suc n = suc (n + 0)
+--     (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
+--       -- (suc n) + 0 = suc n
+--       (plus_0_r (suc n))
+--
+--       -- suc n = suc (n + 0)
+--       (eq_cong nat nat n (plus n zero) suc
+--         -- n = n + 0
+--         (eq_sym nat (plus n zero) n (plus_0_r n))))
+--
+--     -- inductive case
+--     -- IH = suc n + m = suc (n + m)
+--     (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) =>
+--         -- WTS suc n + suc m = suc (n + suc m)
+--         -- suc n + suc m = suc (suc n + m)
+--         --               = suc (suc (n + m))
+--         --               = suc (n + suc m)
+--         (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m)))
+--           -- suc n + suc m = suc (suc n + m)
+--           (plus_s_r (suc n) m)
+--
+--           -- suc (suc n + m) = suc (n + suc m)
+--           (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
+--             -- suc (suc n + m) = suc (suc (n + m))
+--             (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
+--
+--             -- suc (suc (n + m)) = suc (n + suc m)
+--             (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
+--               -- suc (n + m) = n + suc m
+--               (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
+--
+-- -- Finally, we can prove commutativity.
+-- plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
+--   -- As usual, we proceed by induction.
+--   nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
+--
+--   -- Base case: WTS n + 0 = 0 + n
+--   -- n + 0 = n = 0 + n
+--   (eq_trans nat (plus n zero) n (plus zero n)
+--     -- n + 0 = n
+--     (plus_0_r n)
+--
+--     -- n = 0 + n
+--     (eq_sym nat (plus zero n) n (plus_0_l n)))
+--
+--   -- Inductive step:
+--   (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
+--     -- WTS n + suc m = suc m + n
+--     -- n + suc m = suc (n + m)
+--     --           = suc (m + n)
+--     --           = suc m + n
+--     (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
+--       -- n + suc m = suc (n + m)
+--       (plus_s_r n m)
+--
+--       -- suc (n + m) = suc m + n
+--       (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
+--         -- suc (n + m) = suc (m + n)
+--         (eq_cong nat nat (plus n m) (plus m n) suc IH)
+--
+--         -- suc (m + n) = suc m + n
+--         (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));
diff --git a/lib/Check.hs b/lib/Check.hs
index 184817f..49c7bab 100644
--- a/lib/Check.hs
+++ b/lib/Check.hs
@@ -49,11 +49,11 @@ findType g (Abs x a m) = do
 findType g (Pi _ a b) = do
     validateType_ g a
     validateType (incIndices a : map incIndices g) b
-findType g (Let _ v b) = do
-    a <- findType g v
-    validateType_ g a
-    res <- findType (incIndices a : map incIndices g) b
-    pure $ subst 0 a res
+findType g (Let _ v b) = findType g (subst 0 v b)
+    -- a <- findType g v
+    -- validateType_ g a
+    -- res <- findType (incIndices a : map incIndices g) b
+    -- pure $ subst 0 a res
 
 -- this is kinda goofy, it's just like a function, except the resulting type
 -- of the body doesn't need to result in a valid function type
diff --git a/lib/Eval.hs b/lib/Eval.hs
index babf2a9..a94f944 100644
--- a/lib/Eval.hs
+++ b/lib/Eval.hs
@@ -99,6 +99,8 @@ betaEquiv e1 e2
             (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
+            (Let _ v b, e) -> betaEquiv (subst 0 v b) e
+            (e, Let _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible or false
 
 checkBeta :: Env -> Expr -> Expr -> Result Bool