diff --git a/examples/pair.mltt b/examples/pair.mltt
index 1e822525..640e1561 100644
--- a/examples/pair.mltt
+++ b/examples/pair.mltt
@@ -1,11 +1,23 @@
 (
-  (fun (Pair : forall (A : Type@0) (B : Type@0) -> Type@1)
-       (fst : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> A)
-       (snd : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> B)
-       (p : Pair Nat (forall (x : Nat) -> Nat)) ->
-     snd Nat (forall (x : Nat) -> Nat) p (fst Nat (forall (x : Nat) -> Nat) p))
-  (fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C)
-  (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C) -> p A (fun (a : A) (b : B) -> a))
-  (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C) -> p B (fun (a : A) (b : B) -> b))
-  (fun (C : Type@0) (cons : forall (a : Nat) (b : forall (x : Nat) -> Nat) -> C) -> cons 3 (fun (x : Nat) -> succ x))
+  (* Main example *)
+  (
+    fun (Pair : forall (A : Type@0) (B : Type@0) -> Type@1)
+        (pair : forall (A : Type@0) (B : Type@0) (a : A) (b : B) -> Pair A B)
+        (fst : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> A)
+        (snd : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> B) ->
+      (
+        fun (p : Pair Nat (forall (x : Nat) -> Nat)) ->
+          snd Nat (forall (x : Nat) -> Nat) p
+            (fst Nat (forall (x : Nat) -> Nat) p)
+      )
+      (pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x)))
+  )
+  (* Church pair *)
+  (fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C)
+  (* Church pair constructor *)
+  (fun (A : Type@0) (B : Type@0) (a : A) (b : B) (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> pair a b)
+  (* Church pair fst *)
+  (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p A (fun (a : A) (b : B) -> a))
+  (* Church pair snd *)
+  (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p B (fun (a : A) (b : B) -> b))
 ) : Nat
diff --git a/examples/vector.mltt b/examples/vector.mltt
new file mode 100644
index 00000000..5cd1bd14
--- /dev/null
+++ b/examples/vector.mltt
@@ -0,0 +1,41 @@
+(
+  (* Main example *)
+  (
+    fun (Vec : forall (A : Type@0) (n : Nat) -> Type@2)
+        (nil : forall (A : Type@0) -> Vec A 0)
+        (cons : forall (A : Type@0) (n : Nat) (head : A) (tail : Vec A n) -> Vec A (succ n))
+        (vecRec : forall (A : Type@0) (n : Nat) (vec : Vec A n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) ->
+      (
+        fun (totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A)
+            (vec : Vec (forall (n : Nat) -> Nat) 3) ->
+          totalHead ((forall (n : Nat) -> Nat)) 2 vec 4
+      )
+      (* total head function *)
+      (
+        fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) ->
+          vecRec A (succ n) vec (fun (l : Nat) -> rec l return r -> Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r -> Type@0 | zero => Nat | succ l, r => A end) -> a)
+      )
+      (* example vector *)
+      (
+        cons (forall (n : Nat) -> Nat) 2
+          (fun (n : Nat) -> succ (succ (succ n)))
+          (
+            cons (forall (n : Nat) -> Nat) 1
+              (fun (n : Nat) -> succ n)
+              (
+                cons (forall (n : Nat) -> Nat) 0
+                  (fun (n : Nat) -> succ (succ n))
+                  (nil (forall (n : Nat) -> Nat))
+              )
+          )
+      )
+  )
+  (* Church vector *)
+  (fun (A : Type@0) (n : Nat) -> forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n)
+  (* Church vector nil *)
+  (fun (A : Type@0) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> nil)
+  (* Church vector cons *)
+  (fun (A : Type@0) (n : Nat) (head : A) (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> cons n head (tail C nil cons))
+  (* Church vector recursor *)
+  (fun (A : Type@0) (n : Nat) (vec : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> vec C nil cons)
+) : Nat