diff --git a/.gitignore b/.gitignore
index c916390c..a649a8de 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@ plans.txt
 demo/
 .fill.tmp
 .check.hs
+guide.txt
diff --git a/book/Equal.apply.kind2 b/book/Equal.apply.kind2
index 96fd1dba..1d2ab0f8 100644
--- a/book/Equal.apply.kind2
+++ b/book/Equal.apply.kind2
@@ -1,5 +1,17 @@
-Equal.apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: (Equal A a b))
-: (Equal B (f a) (f b))
-= match e {
-    Equal.refl: (Equal.refl _ _)
+use Equal.{refl}
+
+apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
+  match e {
+    refl: {=}
   }
+
+//Equal.apply
+//: ∀(A: *)
+  //∀(B: *)
+  //∀(f: ∀(x: A) B)
+  //∀(a: A)
+  //∀(b: A)
+  //∀(e: (Equal A a b))
+  //(Equal B (f a) (f b))
+//= λA λB λf λa λb λe
+  //(e λx (Equal B (f a) (f x)) λP λx x)
diff --git a/book/List.concat.kind2 b/book/List.concat.kind2
index 0d3e698d..fad8bc32 100644
--- a/book/List.concat.kind2
+++ b/book/List.concat.kind2
@@ -1,8 +1,7 @@
-List.concat
-: ∀(T: *) ∀(xs: (List T)) ∀(ys: (List T)) (List T)
-= λT λxs λys
-  use P = λxs ∀(ys: (List T)) (List T)
-  use cons = λhead λtail λys
-    (List.cons T head (List.concat T tail ys))
-  use nil = λys ys
-  (~xs P cons nil ys)
\ No newline at end of file
+use List.{cons,nil}
+
+concat (T: *) (xs: (List T)) (ys: (List T)) : (List T) =
+  match xs {
+    cons: (cons T xs.head (concat T xs.tail ys))
+    nil: ys
+  }
diff --git a/book/Nat.add.kind2 b/book/Nat.add.kind2
new file mode 100644
index 00000000..fa8a1474
--- /dev/null
+++ b/book/Nat.add.kind2
@@ -0,0 +1,7 @@
+use Nat.{succ,zero}
+
+add (a: Nat) (b: Nat) : Nat =
+  match a {
+    succ: (succ (add a.pred b))
+    zero: b
+  }
diff --git a/book/Nat.lemma.bft.kind2 b/book/Nat.lemma.bft.kind2
index 333cdb35..14c4a879 100644
--- a/book/Nat.lemma.bft.kind2
+++ b/book/Nat.lemma.bft.kind2
@@ -1,16 +1,33 @@
-Nat.lemma.bft
-: ∀(n: Nat) (Equal Nat (Nat.half (Nat.double n)) n)
-= λn
-  (~n
-    λx (Equal Nat (Nat.half (Nat.double x)) x)
-    λn
-    (Equal.apply
-      Nat
-      Nat
-      Nat.succ
-      (Nat.half (Nat.double n))
-      n
-      (Nat.lemma.bft n)
-    )
-    λP λa a
-  )
\ No newline at end of file
+use Nat.{succ,zero,half,double}
+
+bft (n: Nat) : (Equal Nat (half (double n)) n) =
+  match n {
+    succ:
+      let ind = (bft n.pred)
+      let prf = (Equal.apply Nat Nat succ (half (double n.pred)) n.pred ind)
+      prf
+    zero: {=}
+  }
+
+//#found{a
+  //(((Equal (_)) (Nat.succ {n.pred: Nat})) (Nat.half (Nat.double {(Nat.succ {n.pred: Nat}): Nat})))
+  //[
+    //{n: Nat}
+    //λn (((Equal (_)) n) (Nat.half (Nat.double {n: Nat})))
+    //{n.pred: Nat}
+    //{ind: (((Equal (_)) (Nat.half (Nat.double n.pred))) n.pred)}
+  //]}
+
+  //(~n
+    //λx (Equal Nat (Nat.half (Nat.double x)) x)
+    //λn
+    //(Equal.apply
+      //Nat
+      //Nat
+      //Nat.succ
+      //(Nat.half (Nat.double n))
+      //n
+      //(Nat.lemma.bft n)
+    //)
+    //λP λa a
+  //)
diff --git a/book/Vector.concat.kind2 b/book/Vector.concat.kind2
new file mode 100644
index 00000000..9b541d52
--- /dev/null
+++ b/book/Vector.concat.kind2
@@ -0,0 +1,22 @@
+use Vector.{cons,nil}
+use Nat.{succ,zero,add}
+
+concat T (xs_len: Nat) (ys_len: Nat)
+  (xs: (Vector T xs_len))
+  (ys: (Vector T ys_len))
+: (Vector T (add xs_len ys_len))
+= match xs {
+    cons : (cons T (add xs.len ys_len) xs.head (concat T xs.len ys_len xs.tail ys))
+    nil  : ys
+  }
+
+//concat
+//: ∀(T: *)
+  //∀(xs_len: Nat) ∀(xs: (Vector T xs_len))
+  //∀(ys_len: Nat) ∀(ys: (Vector T ys_len))
+  //(Vector T (add xs_len ys_len))
+//= λT λxs_len λxs λys_len λys
+  //(~xs _
+  //λxs.len λxs.head λxs.tail
+    //(Vector.cons T (Nat.add xs.len ys_len) xs.head (concat T xs.len xs.tail ys_len ys))
+  //ys)
diff --git a/book/_main.kind2 b/book/_main.kind2
index f625d8c5..f4028451 100644
--- a/book/_main.kind2
+++ b/book/_main.kind2
@@ -5,7 +5,7 @@
 //use Nat.{succ,zero}
 
 _main : Nat =
-  (Nat.add 1 2)
+  (Nat.half (Nat.double 3))
   
 
 //_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index 00000000..b62cd65d
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,4 @@
+Kind2's Formal Verification!
+----------------------------
+
+Here, we verify the soundness and consistency of Kind2's Core.
diff --git a/formal/kind2.agda b/formal/kind2.agda
new file mode 100644
index 00000000..98cf9802
--- /dev/null
+++ b/formal/kind2.agda
@@ -0,0 +1 @@
+-- TODO :D
diff --git a/src/kind2.hs b/src/kind2.hs
index d453b253..da166cd1 100644
--- a/src/kind2.hs
+++ b/src/kind2.hs
@@ -362,7 +362,7 @@ termSimilar (All aNam aInp aBod) (All bNam bInp bBod) dep = do
 termSimilar (Lam aNam aBod) (Lam bNam bBod) dep =
   termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
 termSimilar (App aFun aArg) (App bFun bArg) dep = do
-  eFun <- termEqual aFun bFun dep
+  eFun <- termSimilar aFun bFun dep
   eArg <- termEqual aArg bArg dep
   envPure (eFun && eArg)
 termSimilar (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
@@ -381,7 +381,7 @@ termSimilar (Mat aNam aX aZ aS aP) (Mat bNam bX bZ bS bP) dep = do
   eS <- termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep
   eP <- termEqual (aP (Var aNam dep)) (bP (Var bNam dep)) dep
   envPure (eX && eZ && eS && eP)
-termSimilar a b dep = envPure False
+termSimilar a b dep = termIdentical a b dep
 
 termIdentical :: Term -> Term -> Int -> Env Bool
 termIdentical a b dep = termIdenticalGo a b dep
diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs
index 8d2fb222..c9202457 100644
--- a/src/sugar/mod.rs
+++ b/src/sugar/mod.rs
@@ -333,12 +333,12 @@ impl Term {
   // - (EQUAL a b) ::= (App (App (App (Var "Equal") _) a) b)
   pub fn as_equal(&self) -> Option<Equal> {
     match self {
-      Term::App { fun, arg } => {
-        if let Term::App { fun: eq_fun, arg: rhs } = &**fun {
+      Term::App { fun, arg: rhs } => {
+        if let Term::App { fun: eq_fun, arg: lhs } = &**fun {
           if let Term::App { fun: eq_fun, arg: _ } = &**eq_fun {
             if let Term::Var { nam } = &**eq_fun {
               if nam == "Equal" {
-                return Some(Equal { a: (**arg).clone(), b: (**rhs).clone() });
+                return Some(Equal { a: (**lhs).clone(), b: (**rhs).clone() });
               }
             }
           }
@@ -403,7 +403,6 @@ impl Term {
 
   // Interprets a λ-encoded Algebraic Data Type definition as an ADT struct.
   pub fn as_adt(&self) -> Option<ADT> {
-
     let name: String;
     let pvar: String;
 
@@ -538,12 +537,12 @@ impl Term {
     let mut self_type = Term::Var { nam: adt.name.clone() };
 
     // Then appends each type parameter
-    for par in adt.pars.iter().rev() {
+    for par in adt.pars.iter() {
       self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par.clone() }) };
     }
 
     // And finally appends each index
-    for (idx_name, _) in adt.idxs.iter().rev() {
+    for (idx_name, _) in adt.idxs.iter() {
       self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: idx_name.clone() }) };
     }