diff --git a/.github/Dockerfile b/.github/Dockerfile
index 28ce8fd5..fb389090 100644
--- a/.github/Dockerfile
+++ b/.github/Dockerfile
@@ -6,5 +6,8 @@ ENV OPAMJOBS=$NCPUS
 
 RUN opam repo add coq-released https://coq.inria.fr/opam/released \
     && opam update \
-    && opam install coq-equations coq-menhirlib menhir ppx_inline_test \
+    && opam install coq-equations coq-menhirlib menhir ppx_expect \
     && eval $(opam env)
+
+RUN sudo apt-get update -y -q \
+    && DEBIAN_FRONTEND=noninteractive sudo apt-get install -y -q --no-install-recommends pandoc
diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml
index 7443cef9..b53c0407 100644
--- a/.github/workflows/ci_build.yaml
+++ b/.github/workflows/ci_build.yaml
@@ -3,9 +3,11 @@ on:
   push:
     branches:
       - main
+      - ext/**
   pull_request:
     branches:
       - main
+      - ext/**
   workflow_dispatch:
   
 permissions:
@@ -71,12 +73,14 @@ jobs:
             endGroup
           script: |
             startGroup "Build binary"
+              make pretty-timed
               if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
                 make coqdoc
-              else
-                make
               fi
             endGroup
+            startGroup "Run inline tests"
+              dune runtest
+            endGroup
           after_script: |
             startGroup "after"
             endGroup
diff --git a/.gitignore b/.gitignore
index b3928d05..3b9fdc1b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 _build
+*.opam
 
 # Ignore generated parser code
 **/parser.ml
diff --git a/.ocamlformat b/.ocamlformat
index 42476c94..4b37f756 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,2 +1,8 @@
 profile = default
-version = 0.24.1
+version = 0.26.2
+
+break-fun-decl = fit-or-vertical
+break-fun-sig = fit-or-vertical
+cases-exp-indent = 3
+exp-grouping = preserve
+if-then-else = keyword-first
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 00000000..0014b174
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 the CompLogic group, Mcgill University
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Makefile b/Makefile
index a690d785..f91fb122 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,14 @@
-.PHONY: all clean
+.PHONY: all pretty-timed test coqdoc clean
 
 all:
 	@$(MAKE) -C theories
 	@dune build
 
-coqdoc: all
+pretty-timed:
+	@$(MAKE) pretty-timed -C theories
+	@dune build
+
+coqdoc:
 	@${MAKE} coqdoc -C theories
 
 clean:
diff --git a/README.md b/README.md
index c2c90121..931ff3e2 100644
--- a/README.md
+++ b/README.md
@@ -79,6 +79,10 @@ possible.
 
 Once `make` finishes, you can run the binary:
 ```
+dune exec mcltt examples/nary.mcl # or your own example
+```
+or more directly
+```
 _build/default/driver/mcltt.exe examples/nary.mcl # or your own example
 ```
 
@@ -88,3 +92,10 @@ cd theories
 make
 ```
 
+## Branches
+
+The Github repo includes the following special branches:
+
+1. `main`: the main branch that is used to generate this homepage and Coqdoc;
+2. `ext/*`: branches in this pattern are variations of `main` that implements various extensions. They are often used to implement extensions that require non-trivial workload and are aimed to be merged to `main` eventually;
+3. `gh-pages`: the branch to host the homepage.
diff --git a/assets/extra/header.html b/assets/extra/header.html
index 98ff925f..3249b6cf 100644
--- a/assets/extra/header.html
+++ b/assets/extra/header.html
@@ -18,7 +18,7 @@
     <span class="button" id="toggle-proofs"></span>
 
     <span class="right">
-      <a href="../">Project Page</a>
+      <a href="./">Project Page</a>
       <a href="./indexpage.html"> Index </a>
       <a href="./toc.html"> Table of Contents </a>
     </span>
diff --git a/driver/Lexer.mli b/driver/Lexer.mli
new file mode 100644
index 00000000..c3a2e915
--- /dev/null
+++ b/driver/Lexer.mli
@@ -0,0 +1,7 @@
+val format_position : Format.formatter -> Lexing.position -> unit
+val format_range : Format.formatter -> Lexing.position * Lexing.position -> unit
+val format_token : Format.formatter -> MclttExtracted.Parser.token -> unit
+val read : Lexing.lexbuf -> MclttExtracted.Parser.token
+
+val lexbuf_to_token_buffer :
+  Lexing.lexbuf -> MclttExtracted.Parser.MenhirLibParser.Inter.buffer
diff --git a/driver/Lexer.mll b/driver/Lexer.mll
index cd92ae95..b590befb 100644
--- a/driver/Lexer.mll
+++ b/driver/Lexer.mll
@@ -104,3 +104,14 @@ and comment =
   parse
   | "*)" { read lexbuf }
   | _ { comment lexbuf }
+
+{
+  let rec lexbuf_to_token_buffer lexbuf =
+    lazy
+      begin
+        try
+          MenhirLibParser.Inter.Buf_cons (read lexbuf, lexbuf_to_token_buffer lexbuf)
+        with
+        | Failure s -> prerr_string s; raise Exit
+      end
+}
diff --git a/driver/Main.ml b/driver/Main.ml
index 5b847973..0859dbb5 100644
--- a/driver/Main.ml
+++ b/driver/Main.ml
@@ -4,26 +4,23 @@ open Parser
 open MenhirLibParser.Inter
 open Entrypoint
 
-let main ?(default_fp = "") () =
-  let fp =
-    if default_fp <> ""
-    then default_fp
-    else
-      begin
-        print_string "File path to load: ";
-        read_line ()
-      end
-  in
-  let chan = open_in fp in
-  (* Before parsing, we must generate a token stream from a lexer buffer,
-     which we then feed into the parser. *)
-  let rec loop lexbuf =
-    lazy (
-        try
-          Buf_cons (Lexer.read lexbuf, loop lexbuf)
-        with
-        | Failure s -> prerr_string s; raise Exit) in
-  let token_stream = loop (Lexing.from_channel chan) in
-  let res = Entrypoint.main 500 token_stream in
-  Format.printf "%a@."
-    PrettyPrinter.format_main_result res
+let get_exit_code result : int =
+  match result with
+  | AllGood _ -> 0
+  | TypeCheckingFailure _ -> 1
+  | ElaborationFailure _ -> 2
+  | ParserFailure _ -> 3
+  | ParserTimeout _ -> 4
+
+let main_of_lexbuf lexbuf =
+  Lexer.lexbuf_to_token_buffer lexbuf
+  (* Here, the integer argument is a *log* version of fuel.
+     Thus, 500 means 2^500. *)
+  |> Entrypoint.main 500
+  |> fun r -> Format.printf "%a@." PrettyPrinter.format_main_result r; get_exit_code r
+
+let main_of_filename filename =
+  Lexing.from_channel (open_in filename) |> main_of_lexbuf
+
+let main_of_program_string program =
+  Lexing.from_string program |> main_of_lexbuf
diff --git a/driver/Main.mli b/driver/Main.mli
new file mode 100644
index 00000000..44046b52
--- /dev/null
+++ b/driver/Main.mli
@@ -0,0 +1,2 @@
+val main_of_filename : string -> int
+val main_of_program_string : string -> int
diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
index 816004bf..b3ebaa50 100644
--- a/driver/Mcltt.ml
+++ b/driver/Mcltt.ml
@@ -1,10 +1,12 @@
 open Mcltt.Main
 
 let () =
-  if Array.length Sys.argv <> 2 then
-    begin
-      Printf.fprintf stderr "incorrect input: %s <input-file>\n" Sys.argv.(0);
-      exit 1
-    end;
+  if Array.length Sys.argv <> 2
+  then begin
+    Printf.fprintf stderr
+      "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
+    exit 5
+  end;
   let filename = Sys.argv.(1) in
-  main ~default_fp:filename ()
+  let code = main_of_filename filename in
+  exit code
diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml
index dcb3f873..5ffdb518 100644
--- a/driver/PrettyPrinter.ml
+++ b/driver/PrettyPrinter.ml
@@ -1,6 +1,5 @@
 open MclttExtracted.Entrypoint
 open MclttExtracted.Syntax
-
 module Parser = MclttExtracted.Parser
 module ParserMessages = MclttExtracted.ParserMessages
 
@@ -8,72 +7,68 @@ module ParserMessages = MclttExtracted.ParserMessages
 (* Formatting helpers *)
 (************************************************************)
 
-let pp_print_paren_if (cond: bool) (body: Format.formatter -> unit -> unit) (f: Format.formatter) (): unit =
-  (if cond then Format.pp_print_char f '(');
+let pp_print_paren_if
+    (cond : bool)
+    (body : Format.formatter -> unit -> unit)
+    (f : Format.formatter)
+    () : unit =
+  if cond then Format.pp_print_char f '(';
   body f ();
-  (if cond then Format.pp_print_char f ')')
+  if cond then Format.pp_print_char f ')'
 
 (************************************************************)
 (* Formatting Cst.obj *)
 (************************************************************)
-let rec get_nat_of_obj: Cst.obj -> int option =
-  function
-  | Cst.Coq_zero   -> Some 0
-  | Cst.Coq_succ e -> Option.map ((+) 1) (get_nat_of_obj e)
-  | _              -> None
+let rec get_nat_of_obj : Cst.obj -> int option = function
+  | Cst.Coq_zero -> Some 0
+  | Cst.Coq_succ e -> Option.map (( + ) 1) (get_nat_of_obj e)
+  | _ -> None
 
-let rec get_fn_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj =
+let rec get_fn_params_of_obj : Cst.obj -> (string * Cst.obj) list * Cst.obj =
   function
   | Cst.Coq_fn (px, ep, ebody) ->
      let params, ebody' = get_fn_params_of_obj ebody in
      ((px, ep) :: params, ebody')
-  | ebody                      -> ([], ebody)
+  | ebody -> ([], ebody)
 
-let rec get_pi_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj =
+let rec get_pi_params_of_obj : Cst.obj -> (string * Cst.obj) list * Cst.obj =
   function
   | Cst.Coq_pi (px, ep, eret) ->
      let params, eret' = get_pi_params_of_obj eret in
      ((px, ep) :: params, eret')
-  | eret                      -> ([], eret)
+  | eret -> ([], eret)
 
-let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
+let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
   let open Format in
   function
-  | Cst.Coq_typ i                                 -> fprintf f "Type@%d" i
-  | Cst.Coq_nat                                   -> fprintf f "Nat"
-  | Cst.Coq_zero                                  -> fprintf f "0"
-  | Cst.Coq_succ e                                ->
-     begin
-       match get_nat_of_obj e with
-       | Some n -> fprintf f "%d" (1 + n)
-       | None   ->
-          let impl f () = fprintf f "succ@ %a" (format_obj_prec 2) e in
-          pp_open_hovbox f 2;
-          pp_print_paren_if (p >= 2) impl f ();
-          pp_close_box f ()
-     end
+  | Cst.Coq_typ i -> fprintf f "Type@%d" i
+  | Cst.Coq_nat -> fprintf f "Nat"
+  | Cst.Coq_zero -> fprintf f "0"
+  | Cst.Coq_succ e -> begin
+     match get_nat_of_obj e with
+     | Some n -> fprintf f "%d" (1 + n)
+     | None ->
+        let impl f () = fprintf f "succ@ %a" (format_obj_prec 2) e in
+        pp_open_hovbox f 2;
+        pp_print_paren_if (p >= 2) impl f ();
+        pp_close_box f ()
+   end
   | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) ->
      let impl f () =
-       fprintf f "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
-         format_obj escr
-         mx
-         format_obj em
-         format_obj ez
-         sx
-         sr
-         format_obj es
+       fprintf f
+         "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ \
+          %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
+         format_obj escr mx format_obj em format_obj ez sx sr format_obj es
      in
      pp_print_paren_if (p >= 1) impl f ()
-  | Cst.Coq_app (ef, ea)                          ->
+  | Cst.Coq_app (ef, ea) ->
      let impl f () =
-       fprintf f "%a@ %a"
-         (format_obj_prec 1) ef
-         (format_obj_prec 2) ea;
+       fprintf f "%a@ %a" (format_obj_prec 1) ef (format_obj_prec 2) ea
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 2) impl f ();
      pp_close_box f ()
-  | Cst.Coq_fn (px, ep, ebody)                    ->
+  | Cst.Coq_fn (px, ep, ebody) ->
      let params, ebody' = get_fn_params_of_obj ebody in
      let impl f () =
        pp_print_string f "fun ";
@@ -86,13 +81,12 @@ let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]"
-         format_obj ebody'
+       fprintf f "-> @[<hov 2>%a@]" format_obj ebody'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_pi (px, ep, eret)                     ->
+  | Cst.Coq_pi (px, ep, eret) ->
      let params, eret' = get_pi_params_of_obj eret in
      let impl f () =
        pp_print_string f "forall ";
@@ -105,65 +99,70 @@ let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]"
-         format_obj eret'
+       fprintf f "-> @[<hov 2>%a@]" format_obj eret'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_var x                                 -> pp_print_string f x
-and format_obj_param f (px, ep) =
-  Format.fprintf f "(%s : %a)"
-    px
-    format_obj ep
+  | Cst.Coq_var x -> pp_print_string f x
+
+and format_obj_param f (px, ep) = Format.fprintf f "(%s : %a)" px format_obj ep
 and format_obj f = format_obj_prec 0 f
 
 (************************************************************)
 (* Formatting exp *)
 (************************************************************)
 let exp_to_obj =
-  let new_var =
+  let new_var, reset_var_suffix =
     let suffix = ref 0 in
-    fun () ->
-    incr suffix;
-    "x" ^ string_of_int !suffix
+    ( (fun () ->
+        incr suffix;
+        "x" ^ string_of_int !suffix),
+      fun () -> suffix := 0 )
   in
-  let new_tyvar =
+  let new_tyvar, reset_tyvar_suffix =
     let suffix = ref 0 in
-    fun () ->
-    incr suffix;
-    "A" ^ string_of_int !suffix
+    ( (fun () ->
+        incr suffix;
+        "A" ^ string_of_int !suffix),
+      fun () -> suffix := 0 )
   in
-  let rec impl (ctx: string list): exp -> Cst.obj =
-    function
+  let rec impl (ctx : string list) : exp -> Cst.obj = function
     | Coq_a_zero -> Cst.Coq_zero
     | Coq_a_succ e -> Cst.Coq_succ (impl ctx e)
     | Coq_a_natrec (em, ez, es, escr) ->
-       let mx, sx, sr = new_var (), new_var (), new_var () in
-       Cst.Coq_natrec (impl ctx escr, mx, impl (mx :: ctx) em, impl ctx ez, sx, sr, impl (sr :: sx :: ctx) es)
+       let mx = new_var () in
+       let sx = new_var () in
+       let sr = match em with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let escr' = impl ctx escr in
+       let em' = impl (mx :: ctx) em in
+       let ez' = impl ctx ez in
+       let es' = impl (sr :: sx :: ctx) es in
+       Cst.Coq_natrec (escr', mx, em', ez', sx, sr, es')
     | Coq_a_nat -> Cst.Coq_nat
     | Coq_a_typ i -> Cst.Coq_typ i
     | Coq_a_var x -> Cst.Coq_var (List.nth ctx x)
     | Coq_a_fn (ep, ebody) ->
-       let px =
-         match ep with
-         | Coq_a_typ _ -> new_tyvar ()
-         | _           -> new_var ()
-       in
-       Cst.Coq_fn (px, impl ctx ep, impl (px :: ctx) ebody)
+       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let ep' = impl ctx ep in
+       let ebody' = impl (px :: ctx) ebody in
+       Cst.Coq_fn (px, ep', ebody')
     | Coq_a_app (ef, ea) ->
-       Cst.Coq_app (impl ctx ef, impl ctx ea)
+       let ef' = impl ctx ef in
+       let ea' = impl ctx ea in
+       Cst.Coq_app (ef', ea')
     | Coq_a_pi (ep, eret) ->
-       let px =
-         match ep with
-         | Coq_a_typ _ -> new_tyvar ()
-         | _           -> new_var ()
-       in
-       Cst.Coq_pi (px, impl ctx ep, impl (px :: ctx) eret)
+       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let ep' = impl ctx ep in
+       let eret' = impl (px :: ctx) eret in
+       Cst.Coq_pi (px, ep', eret')
     | Coq_a_sub _ -> failwith "Invalid internal language construct"
   in
-  impl []
-  
+  fun exp ->
+    reset_var_suffix ();
+    reset_tyvar_suffix ();
+    impl [] exp
+
 let format_exp f exp = format_obj f (exp_to_obj exp)
 
 (************************************************************)
@@ -176,32 +175,26 @@ let format_nf f nf = format_exp f (nf_to_exp nf)
 (* Formatting main_result *)
 (************************************************************)
 
-let format_main_result (f: Format.formatter): main_result -> unit =
+let format_main_result (f : Format.formatter) : main_result -> unit =
   let open Format in
   function
   | AllGood (cst_typ, cst_exp, typ, exp, nf) ->
-     fprintf f "@[<v 2>Parsed:@ @[<hv 0>%a@ : %a@]@]"
-       format_obj cst_exp
+     fprintf f "@[<v 2>Parsed:@ @[<hv 0>%a@ : %a@]@]" format_obj cst_exp
        format_obj cst_typ;
      pp_force_newline f ();
-     fprintf f "@[<v 2>Elaborated:@ @[<hv 0>%a@ : %a@]@]"
-       format_exp exp
+     fprintf f "@[<v 2>Elaborated:@ @[<hv 0>%a@ : %a@]@]" format_exp exp
        format_exp typ;
      pp_force_newline f ();
-     fprintf f "@[<v 2>Normalized Result:@ @[<hv 0>%a@ : %a@]@]"
-       format_nf nf
+     fprintf f "@[<v 2>Normalized Result:@ @[<hv 0>%a@ : %a@]@]" format_nf nf
        format_exp typ
   | TypeCheckingFailure (typ, exp) ->
      printf "@[<v 2>Type Checking Failure:@ %a@;<1 -2>is not of@ %a@]"
-       format_exp exp
-       format_exp typ
+       format_exp exp format_exp typ
   | ElaborationFailure cst_exp ->
      printf "@[<v 2>Elaboration Failure:@ %a@;<1 -2>cannot be elaborated@]"
        format_obj cst_exp
   | ParserFailure (s, t) ->
      printf "@[<v 2>Parser Failure:@ on %a:@ @ @[<hov 0>%a@]@]"
-       Lexer.format_token t
-       pp_print_text (ParserMessages.message (Parser.Aut.coq_N_of_state s))
-  | ParserTimeout fuel ->
-     printf "@[<v 2>Parser Timeout with Fuel %d@]"
-       fuel
+       Lexer.format_token t pp_print_text
+       (ParserMessages.message (Parser.Aut.coq_N_of_state s))
+  | ParserTimeout fuel -> printf "@[<v 2>Parser Timeout with Fuel %d@]" fuel
diff --git a/driver/PrettyPrinter.mli b/driver/PrettyPrinter.mli
new file mode 100644
index 00000000..0ceb66b9
--- /dev/null
+++ b/driver/PrettyPrinter.mli
@@ -0,0 +1,6 @@
+val format_obj : Format.formatter -> MclttExtracted.Syntax.Cst.obj -> unit
+val format_exp : Format.formatter -> MclttExtracted.Syntax.exp -> unit
+val format_nf : Format.formatter -> MclttExtracted.Syntax.nf -> unit
+
+val format_main_result :
+  Format.formatter -> MclttExtracted.Entrypoint.main_result -> unit
diff --git a/driver/Test.ml b/driver/Test.ml
index c25b8dcd..475cd810 100644
--- a/driver/Test.ml
+++ b/driver/Test.ml
@@ -1,50 +1,593 @@
 (* Unit test cases for parsing *)
 
 open Main
-open Entrypoint.Cst
+open MclttExtracted.Entrypoint
 
-let x, y, z = ("x", "y", "z")
+(** Helper definitions *)
 
-let%test "type" = parse "Type 5" = Some (Coq_typ 5)
-let%test "nat" = parse "Nat" = Some Coq_nat
-let%test "var" = parse "x" = Some (Coq_var x)
-let%test "zero" = parse "zero" = Some Coq_zero
-let%test "succ zero" = parse "succ zero" = Some (Coq_succ Coq_zero)
+let main_of_example s = main_of_filename ("../examples/" ^ s)
 
-let%test "lambda" =
-  parse "fun (x : Type 5).y" = Some (Coq_fn (x, Coq_typ 5, Coq_var y))
+(** Real tests *)
+(* We never expect parser timeout. 2^500 fuel should be large enough! *)
 
-let%test "lambda multiple args" =
-  parse "fun (x : Nat) (y : Nat) . x"
-  = Some (Coq_fn (x, Coq_nat, Coq_fn (y, Coq_nat, Coq_var x)))
+let%expect_test "Type@0 is of Type@1" =
+  let _ = main_of_program_string "Type@0 : Type@1" in
+  [%expect
+    {|
+    Parsed:
+      Type@0 : Type@1
+    Elaborated:
+      Type@0 : Type@1
+    Normalized Result:
+      Type@0 : Type@1
+  |}]
 
-let%test "lambda multiple args 2" =
-  parse "fun (x : Nat) (y : Nat) (z : Nat) . z"
-  = Some
-      (Coq_fn (x, Coq_nat, Coq_fn (y, Coq_nat, Coq_fn (z, Coq_nat, Coq_var z))))
+let%expect_test "zero is of Nat" =
+  let _ = main_of_program_string "zero : Nat" in
+  [%expect
+    {|
+    Parsed:
+      0 : Nat
+    Elaborated:
+      0 : Nat
+    Normalized Result:
+      0 : Nat
+  |}]
 
-let%test "application" =
-  parse "(fun (x : Nat).x) Nat"
-  = Some (Coq_app (Coq_fn (x, Coq_nat, Coq_var x), Coq_nat))
+let%expect_test "zero is not of Type@0" =
+  let _ = main_of_program_string "zero : Type@0" in
+  [%expect
+    {|
+    Type Checking Failure:
+      0
+    is not of
+      Type@0
+  |}]
 
-let%test "nested 1" =
-  parse "(Type 5) zero" = Some (Coq_app (Coq_typ 5, Coq_zero))
+let%expect_test "succ zero is of Nat" =
+  let _ = main_of_program_string "succ zero : Nat" in
+  [%expect
+    {|
+    Parsed:
+      1 : Nat
+    Elaborated:
+      1 : Nat
+    Normalized Result:
+      1 : Nat
+  |}]
 
-let%test "nested 2" =
-  parse "succ (succ (succ (succ zero)))"
-  = Some (Coq_succ (Coq_succ (Coq_succ (Coq_succ Coq_zero))))
+let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
+  let _ = main_of_program_string "succ Type@0 : Nat" in
+  [%expect
+    {|
+    Type Checking Failure:
+      succ Type@0
+    is not of
+      Nat
+  |}]
 
-let%test "pi" = parse "pi (x:Nat).x" = Some (Coq_pi (x, Coq_nat, Coq_var x))
+let%expect_test "variable x is ill-scoped" =
+  let _ = main_of_program_string "x : Type@0" in
+  [%expect {|
+    Elaboration Failure:
+      x
+    cannot be elaborated
+  |}]
 
-let%test "pi multiple args" =
-  parse "pi (x : Nat) (y : Nat) (z : Nat) . z"
-  = Some
-      (Coq_pi (x, Coq_nat, Coq_pi (y, Coq_nat, Coq_pi (z, Coq_nat, Coq_var z))))
+let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
+  let _ = main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat" in
+  [%expect
+    {|
+    Parsed:
+      fun (y : Nat) -> y : forall (x : Nat) -> Nat
+    Elaborated:
+      fun (x1 : Nat) -> x1 : forall (x1 : Nat) -> Nat
+    Normalized Result:
+      fun (x1 : Nat) -> x1 : forall (x1 : Nat) -> Nat
+  |}]
 
-(* Some more finer details *)
+let%expect_test "recursion on a natural number that always returns zero is of \
+                 Nat" =
+  let _ = main_of_program_string
+    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat" in
+  [%expect
+    {|
+    Parsed:
+      rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat
+    Elaborated:
+      rec 3 return x1 -> Nat | zero => 0 | succ x2, x3 => 0 end : Nat
+    Normalized Result:
+      0 : Nat
+  |}]
 
-let%test "pi missing colon" = parse "pi (x Nat).x" = None
+let%expect_test "simple_nat.mcl works" =
+  let _ = main_of_example "simple_nat.mcl" in
+  [%expect
+    {|
+    Parsed:
+      4 : Nat
+    Elaborated:
+      4 : Nat
+    Normalized Result:
+      4 : Nat
+  |}]
 
-let%test "ignore whitespace" =
-  parse "fun (x  \n                                     : Type 4).x"
-  = Some (Coq_fn (x, Coq_typ 4, Coq_var x))
+let%expect_test "simple_rec.mcl works" =
+  let _ = main_of_example "simple_rec.mcl" in
+  [%expect
+    {|
+    Parsed:
+      fun (x : Nat)
+        -> rec x return y -> Nat | zero => 1 | succ n, r => succ r end
+      : forall (x : Nat) -> Nat
+    Elaborated:
+      fun (x1 : Nat)
+        -> rec x1 return x2 -> Nat | zero => 1 | succ x3, x4 => succ x4 end
+      : forall (x1 : Nat) -> Nat
+    Normalized Result:
+      fun (x1 : Nat)
+        -> rec x1 return x2 -> Nat | zero => 1 | succ x3, x4 => succ x4 end
+      : forall (x1 : Nat) -> Nat
+  |}]
+
+let%expect_test "pair.mcl works" =
+  let _ = main_of_example "pair.mcl" in
+  [%expect
+    {|
+    Parsed:
+      (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))))
+        (fun (A : Type@0)
+             (B : Type@0)
+          -> forall (C : Type@0)
+                    (pair : forall (a : A)
+                                   (b : B)
+                              -> C)
+               -> C)
+        (fun (A : Type@0)
+             (B : Type@0)
+             (a : A)
+             (b : B)
+             (C : Type@0)
+             (pair : forall (a : A)
+                            (b : B)
+                       -> C)
+          -> pair a b)
+        (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))
+        (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
+    Elaborated:
+      (fun (x1 : forall (A1 : Type@0)
+                        (A2 : Type@0)
+                   -> Type@1)
+           (x2 : forall (A3 : Type@0)
+                        (A4 : Type@0)
+                        (x3 : A3)
+                        (x4 : A4)
+                   -> x1 A3 A4)
+           (x5 : forall (A5 : Type@0)
+                        (A6 : Type@0)
+                        (x6 : x1 A5 A6)
+                   -> A5)
+           (x7 : forall (A7 : Type@0)
+                        (A8 : Type@0)
+                        (x8 : x1 A7 A8)
+                   -> A8)
+        -> (fun (x9 : x1 Nat (forall (x10 : Nat) -> Nat))
+             -> x7 Nat (forall (x11 : Nat) -> Nat) x9
+                  (x5 Nat (forall (x12 : Nat) -> Nat) x9))
+             (x2 Nat (forall (x13 : Nat) -> Nat) 3
+               (fun (x14 : Nat) -> succ (succ x14))))
+        (fun (A9 : Type@0)
+             (A10 : Type@0)
+          -> forall (A11 : Type@0)
+                    (x15 : forall (x16 : A9)
+                                  (x17 : A10)
+                             -> A11)
+               -> A11)
+        (fun (A12 : Type@0)
+             (A13 : Type@0)
+             (x18 : A12)
+             (x19 : A13)
+             (A14 : Type@0)
+             (x20 : forall (x21 : A12)
+                           (x22 : A13)
+                      -> A14)
+          -> x20 x18 x19)
+        (fun (A15 : Type@0)
+             (A16 : Type@0)
+             (x23 : forall (A17 : Type@0)
+                           (x24 : forall (x25 : A15)
+                                         (x26 : A16)
+                                    -> A17)
+                      -> A17)
+          -> x23 A15 (fun (x27 : A15)
+                          (x28 : A16)
+                       -> x27))
+        (fun (A18 : Type@0)
+             (A19 : Type@0)
+             (x29 : forall (A20 : Type@0)
+                           (x30 : forall (x31 : A18)
+                                         (x32 : A19)
+                                    -> A20)
+                      -> A20)
+          -> x29 A19 (fun (x33 : A18)
+                          (x34 : A19)
+                       -> x34))
+      : Nat
+    Normalized Result:
+      5 : Nat
+  |}]
+
+let%expect_test "vector.mcl works" =
+  let _ = main_of_example "vector.mcl" in
+  [%expect
+    {|
+    Parsed:
+      (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)
+             (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))
+             (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))))))
+        (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)
+        (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)
+        (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))
+        (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
+    Elaborated:
+      (fun (x1 : forall (A1 : Type@0)
+                        (x2 : Nat)
+                   -> Type@2)
+           (x3 : forall (A2 : Type@0) -> x1 A2 0)
+           (x4 : forall (A3 : Type@0)
+                        (x5 : Nat)
+                        (x6 : A3)
+                        (x7 : x1 A3 x5)
+                   -> x1 A3 (succ x5))
+           (x8 : forall (A4 : Type@0)
+                        (x9 : Nat)
+                        (x10 : x1 A4 x9)
+                        (x11 : forall (x12 : Nat) -> Type@1)
+                        (x13 : x11 0)
+                        (x14 : forall (x15 : Nat)
+                                      (x16 : A4)
+                                      (x17 : x11 x15)
+                                 -> x11 (succ x15))
+                   -> x11 x9)
+        -> (fun (x18 : forall (A5 : Type@0)
+                              (x19 : Nat)
+                              (x20 : x1 A5 (succ x19))
+                         -> A5)
+                (x21 : x1 (forall (x22 : Nat) -> Nat) 3)
+             -> x18 (forall (x23 : Nat) -> Nat) 2 x21 4)
+             (fun (A6 : Type@0)
+                  (x24 : Nat)
+                  (x25 : x1 A6 (succ x24))
+               -> x8 A6 (succ x24) x25
+                    (fun (x26 : Nat)
+                      -> rec x26 return x27 -> Type@0
+                         | zero => Nat
+                         | succ x28, A7 => A6
+                         end)
+                    0
+                    (fun (x29 : Nat)
+                         (x30 : A6)
+                         (x31 : rec x29 return x32 -> Type@0
+                                | zero => Nat
+                                | succ x33, A8 => A6
+                                end)
+                      -> x30))
+             (x4 (forall (x34 : Nat) -> Nat) 2
+                (fun (x35 : Nat) -> succ (succ (succ x35)))
+               (x4 (forall (x36 : Nat) -> Nat) 1 (fun (x37 : Nat) -> succ x37)
+                 (x4 (forall (x38 : Nat) -> Nat) 0
+                    (fun (x39 : Nat) -> succ (succ x39))
+                   (x3 (forall (x40 : Nat) -> Nat))))))
+        (fun (A9 : Type@0)
+             (x41 : Nat)
+          -> forall (x42 : forall (x43 : Nat) -> Type@1)
+                    (x44 : x42 0)
+                    (x45 : forall (x46 : Nat)
+                                  (x47 : A9)
+                                  (x48 : x42 x46)
+                             -> x42 (succ x46))
+               -> x42 x41)
+        (fun (A10 : Type@0)
+             (x49 : forall (x50 : Nat) -> Type@1)
+             (x51 : x49 0)
+             (x52 : forall (x53 : Nat)
+                           (x54 : A10)
+                           (x55 : x49 x53)
+                      -> x49 (succ x53))
+          -> x51)
+        (fun (A11 : Type@0)
+             (x56 : Nat)
+             (x57 : A11)
+             (x58 : forall (x59 : forall (x60 : Nat) -> Type@1)
+                           (x61 : x59 0)
+                           (x62 : forall (x63 : Nat)
+                                         (x64 : A11)
+                                         (x65 : x59 x63)
+                                    -> x59 (succ x63))
+                      -> x59 x56)
+             (x66 : forall (x67 : Nat) -> Type@1)
+             (x68 : x66 0)
+             (x69 : forall (x70 : Nat)
+                           (x71 : A11)
+                           (x72 : x66 x70)
+                      -> x66 (succ x70))
+          -> x69 x56 x57 (x58 x66 x68 x69))
+        (fun (A12 : Type@0)
+             (x73 : Nat)
+             (x74 : forall (x75 : forall (x76 : Nat) -> Type@1)
+                           (x77 : x75 0)
+                           (x78 : forall (x79 : Nat)
+                                         (x80 : A12)
+                                         (x81 : x75 x79)
+                                    -> x75 (succ x79))
+                      -> x75 x73)
+             (x82 : forall (x83 : Nat) -> Type@1)
+             (x84 : x82 0)
+             (x85 : forall (x86 : Nat)
+                           (x87 : A12)
+                           (x88 : x82 x86)
+                      -> x82 (succ x86))
+          -> x74 x82 x84 x85)
+      : Nat
+    Normalized Result:
+      7 : Nat
+  |}]
+
+let%expect_test "nary.mcl works" =
+  let _ = main_of_example "nary.mcl" in
+  [%expect
+    {|
+    Parsed:
+      (fun (Nary : forall (n : Nat) -> Type@0)
+           (toNat : forall (f : Nary 0) -> Nat)
+           (appNary : forall (n : Nat)
+                             (f : Nary (succ n))
+                             (arg : Nat)
+                        -> Nary n)
+           (n : Nat)
+           (f : Nary n)
+        -> (rec n return y -> forall (g : Nary y) -> Nat
+            | zero => toNat
+            | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m))
+            end)
+             f)
+        (fun (n : Nat)
+          -> rec n return y -> Type@0
+             | zero => Nat
+             | succ m, r => forall (a : Nat) -> r
+             end)
+        (fun (f : Nat) -> f)
+        (fun (n : Nat)
+             (f : rec succ n return y -> Type@0
+                  | zero => Nat
+                  | succ m, r => forall (a : Nat) -> r
+                  end)
+             (arg : Nat)
+          -> f arg)
+        3
+        ((fun (add : forall (a : Nat)
+                            (b : Nat)
+                       -> Nat)
+              (a : Nat)
+              (b : Nat)
+              (c : Nat)
+           -> add a (add b c))
+          (fun (a : Nat)
+               (b : Nat)
+            -> rec a return y -> Nat | zero => b | succ m, r => succ r end))
+      : Nat
+    Elaborated:
+      (fun (x1 : forall (x2 : Nat) -> Type@0)
+           (x3 : forall (x4 : x1 0) -> Nat)
+           (x5 : forall (x6 : Nat)
+                        (x7 : x1 (succ x6))
+                        (x8 : Nat)
+                   -> x1 x6)
+           (x9 : Nat)
+           (x10 : x1 x9)
+        -> (rec x9 return x11 -> forall (x14 : x1 x11) -> Nat
+            | zero => x3
+            | succ x12, x13 =>
+              fun (x15 : x1 (succ x12)) -> x13 (x5 x12 x15 (succ x12))
+            end)
+             x10)
+        (fun (x16 : Nat)
+          -> rec x16 return x17 -> Type@0
+             | zero => Nat
+             | succ x18, A1 => forall (x19 : Nat) -> A1
+             end)
+        (fun (x20 : Nat) -> x20)
+        (fun (x21 : Nat)
+             (x22 : rec succ x21 return x23 -> Type@0
+                    | zero => Nat
+                    | succ x24, A2 => forall (x25 : Nat) -> A2
+                    end)
+             (x26 : Nat)
+          -> x22 x26)
+        3
+        ((fun (x27 : forall (x28 : Nat)
+                            (x29 : Nat)
+                       -> Nat)
+              (x30 : Nat)
+              (x31 : Nat)
+              (x32 : Nat)
+           -> x27 x30 (x27 x31 x32))
+          (fun (x33 : Nat)
+               (x34 : Nat)
+            -> rec x33 return x35 -> Nat
+               | zero => x34
+               | succ x36, x37 => succ x37
+               end))
+      : Nat
+    Normalized Result:
+      6 : Nat
+  |}]
+
+(* let%test "lambda" = *)
+(*   parse "fun (x : Type 5).y" = Some (Coq_fn (x, Coq_typ 5, Coq_var y)) *)
+
+(* let%test "lambda multiple args" = *)
+(*   parse "fun (x : Nat) (y : Nat) . x" *)
+(*   = Some (Coq_fn (x, Coq_nat, Coq_fn (y, Coq_nat, Coq_var x))) *)
+
+(* let%test "lambda multiple args 2" = *)
+(*   parse "fun (x : Nat) (y : Nat) (z : Nat) . z" *)
+(*   = Some *)
+(*       (Coq_fn (x, Coq_nat, Coq_fn (y, Coq_nat, Coq_fn (z, Coq_nat, Coq_var z)))) *)
+
+(* let%test "application" = *)
+(*   parse "(fun (x : Nat).x) Nat" *)
+(*   = Some (Coq_app (Coq_fn (x, Coq_nat, Coq_var x), Coq_nat)) *)
+
+(* let%test "nested 1" = *)
+(*   parse "(Type 5) zero" = Some (Coq_app (Coq_typ 5, Coq_zero)) *)
+
+(* let%test "nested 2" = *)
+(*   parse "succ (succ (succ (succ zero)))" *)
+(*   = Some (Coq_succ (Coq_succ (Coq_succ (Coq_succ Coq_zero)))) *)
+
+(* let%test "pi" = parse "pi (x:Nat).x" = Some (Coq_pi (x, Coq_nat, Coq_var x)) *)
+
+(* let%test "pi multiple args" = *)
+(*   parse "pi (x : Nat) (y : Nat) (z : Nat) . z" *)
+(*   = Some *)
+(*       (Coq_pi (x, Coq_nat, Coq_pi (y, Coq_nat, Coq_pi (z, Coq_nat, Coq_var z)))) *)
+
+(* (\* Some more finer details *\) *)
+
+(* let%test "pi missing colon" = parse "pi (x Nat).x" = None *)
+
+(* let%test "ignore whitespace" = *)
+(*   parse "fun (x  \n                                     : Type 4).x" *)
+(*   = Some (Coq_fn (x, Coq_typ 4, Coq_var x)) *)
diff --git a/driver/dune b/driver/dune
index 1a350682..40e0c90a 100644
--- a/driver/dune
+++ b/driver/dune
@@ -2,16 +2,18 @@
 
 (library
  (name Mcltt)
- (public_name mcltt.Driver)
- (modules Main Lexer PrettyPrinter)
+ (public_name mcltt.driver)
+ (modules Main Lexer PrettyPrinter Test)
  (libraries MclttExtracted)
- ; (inline_tests)
- ; (preprocess
- ;  (pps ppx_inline_test))
-)
+ (inline_tests
+  (deps
+   (glob_files_rec ../examples/*.mcl)))
+ (preprocess
+  (pps ppx_expect)))
 
 (executable
  (name mcltt)
+ (public_name mcltt)
  (modules Mcltt)
  (libraries Mcltt))
 
diff --git a/driver/extracted/.ocamlformat b/driver/extracted/.ocamlformat
new file mode 100644
index 00000000..fc8e62b7
--- /dev/null
+++ b/driver/extracted/.ocamlformat
@@ -0,0 +1 @@
+disable = true
\ No newline at end of file
diff --git a/driver/extracted/dune b/driver/extracted/dune
index 233b358d..aa468c51 100644
--- a/driver/extracted/dune
+++ b/driver/extracted/dune
@@ -1,5 +1,5 @@
 (library
  (name MclttExtracted)
- (public_name mcltt.Extracted))
+ (public_name mcltt.extracted))
 
 (documentation)
diff --git a/dune-project b/dune-project
index 88b2a868..e141f18b 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,34 @@
 (lang dune 3.13)
 (using menhir 2.1)
 (name mcltt)
+
+(generate_opam_files)
+
+(license MIT)
+(authors "Antoine Gaulin"
+         "Jason Hu"
+         "Junyoung Jang")
+(maintainers "the CompLogic group, McGill University")
+(homepage "https://beluga-lang.github.io/McLTT/")
+(documentation "https://beluga-lang.github.io/McLTT/")
+(source (github Beluga-lang/McLTT))
+
+(package
+ (name mcltt)
+ (synopsis "A Bottom-up Approach to Implementing A Proof Assistant")
+ (description "In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After
+the accomplishment of this project, we will obtain an executable, to which we can feed
+a program in Martin-Loef type theory, and this executable will check whether this
+program has the specified type. McLTT is novel in that it is implemented in
+Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is
+sound and complete: a program passes typechecking if and only if it is a well-typed
+program in MLTT. This will be the first verified proof assistant (despite being
+elementary) and serves as a basis for future extensions.")
+ (depends
+  (ocaml (>= "4.14.2"))
+  (coq   (= "8.20.0"))
+  (menhir (= "20240715"))
+  (coq-menhirlib (= "20240715"))
+  (coq-equations (= "1.3.1+8.20"))
+  (ppx_expect (>= "0.16.0"))
+  (sherlodoc :with-doc)))
diff --git a/mcltt.opam.template b/mcltt.opam.template
new file mode 100644
index 00000000..3d7af790
--- /dev/null
+++ b/mcltt.opam.template
@@ -0,0 +1,5 @@
+build: [
+  [make]
+  [make coqdoc] {with-doc}
+]
+
diff --git a/theories/CoqMakefile.mk.local-late b/theories/CoqMakefile.mk.local-late
index 336904ec..d0e3ee8a 100644
--- a/theories/CoqMakefile.mk.local-late
+++ b/theories/CoqMakefile.mk.local-late
@@ -6,11 +6,13 @@ MENHIR := menhir
 PARSERMESSAGEBASE := parserMessages.messages
 FRONTENDDIR := Frontend
 PARSERMESSAGEFILE := $(FRONTENDDIR)/$(PARSERMESSAGEBASE)
+PARSERMESSAGETEMPFILE := $(PARSERMESSAGEFILE:%.messages=%.messages.temp)
+PARSERMESSAGEMERGEFILE := $(PARSERMESSAGEFILE:%.messages=%.messages.merge)
 PARSERMESSAGEEXTRACTIONFILE := ../driver/extracted/ParserMessages.ml
 COQPARSERORIGFILE := $(shell find ./ -name '*.vy')
 COQPARSERFILE := $(COQPARSERORIGFILE:%.vy=%.v)
 
-post-all:: $(COQPARSERFILE) $(PARSERMESSAGEEXTRACTIONFILE)
+post-all:: $(COQPARSERFILE) $(PARSERMESSAGEEXTRACTIONFILE) check_parserMessages
 	@echo "Separate Extraction main." | $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile Entrypoint.v -l Entrypoint.v
 
 $(COQPARSERFILE): %.v : %.vy
@@ -18,3 +20,16 @@ $(COQPARSERFILE): %.v : %.vy
 
 $(PARSERMESSAGEEXTRACTIONFILE): $(PARSERMESSAGEFILE) $(COQPARSERORIGFILE)
 	$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compile-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEEXTRACTIONFILE)"
+
+.PHONY: check_parserMessages
+check_parserMessages:
+	$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
+	$(MENHIR) --coq "$(COQPARSERORIGFILE)" --compare-errors "$(PARSERMESSAGETEMPFILE)" --compare-errors "$(PARSERMESSAGEFILE)"
+	rm "$(PARSERMESSAGETEMPFILE)"
+
+.PHONY: update_parserMessages
+update_parserMessages:
+	$(MENHIR) --coq "$(COQPARSERORIGFILE)" --list-errors > "$(PARSERMESSAGETEMPFILE)"
+	$(MENHIR) --coq "$(COQPARSERORIGFILE)" --merge-errors "$(PARSERMESSAGETEMPFILE)" --merge-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEMERGEFILE)"
+	rm "$(PARSERMESSAGETEMPFILE)"
+	mv "$(PARSERMESSAGEMERGEFILE)" "$(PARSERMESSAGEFILE)"
diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
index 597b40c6..b61de31d 100644
--- a/theories/Core/Semantic/PER/CoreTactics.v
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -46,8 +46,7 @@ Ltac destruct_rel_typ :=
 
 Ltac basic_invert_per_univ_elem H :=
   progress simp per_univ_elem in H;
-  inversion H;
-  subst;
+  dependent destruction H;
   try rewrite <- per_univ_elem_equation_1 in *.
 
 Ltac basic_per_univ_elem_econstructor :=
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 826c36ea..f742ff19 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -446,10 +446,10 @@ Lemma per_univ_elem_trans : forall i R a1 a2,
           R m1 m2 ->
           R m2 m3 ->
           R m1 m3).
-Proof with (basic_per_univ_elem_econstructor; mautosolve).
+Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
   induction 1 using per_univ_elem_ind;
     [> split;
-     [ intros * HT2; basic_invert_per_univ_elem HT2; clear HT2
+     [ intros * HT2; basic_invert_per_univ_elem HT2
      | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
   - (* univ case *)
     subst.
diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v
index 8134cf2c..c0b463ce 100644
--- a/theories/Core/Soundness/FunctionCases.v
+++ b/theories/Core/Soundness/FunctionCases.v
@@ -364,7 +364,7 @@ Proof.
   assert {{ Γ ⊩ A : Type@(max i j) }} by mauto 3.
   assert {{ ⊩ Γ, A }} by mauto 2.
   assert (i <= max i j) by lia.
-  assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 3.
+  assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 4.
   assert {{ Γ, A ⊩ B : Type@(max i j) }} by mauto 3.
   mauto 2 using glu_rel_exp_app_helper.
 Qed.
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 976d2247..515bdafa 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -59,7 +59,7 @@ Lemma glu_nat_resp_exp_eq : forall Γ M a,
     {{ Γ ⊢ M ≈ M' : ℕ }} ->
     glu_nat Γ M' a.
 Proof.
-  induction 1; intros; mauto.
+  induction 1; intros; mauto 4.
   econstructor; trivial.
   intros.
   transitivity {{{ M[σ] }}}; mauto.
@@ -82,11 +82,11 @@ Lemma glu_nat_readback : forall Γ M a,
       {{ Δ ⊢ M[σ] ≈ M' : ℕ }}.
 Proof.
   induction 1; intros; progressive_inversion; gen_presups.
-  - transitivity {{{ zero[σ] }}}; mauto.
-  - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto.
+  - transitivity {{{ zero[σ] }}}; mauto 4.
+  - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto 4.
     transitivity {{{ (succ M')[σ] }}}; mauto 3.
     transitivity {{{ succ M'[σ] }}}; mauto 4.
-  - mauto.
+  - mauto 4.
 Qed.
 
 #[global]
@@ -270,7 +270,7 @@ Lemma glu_univ_elem_per_elem : forall i P El a,
 Proof.
   simpl.
   induction 1 using glu_univ_elem_ind; intros;
-    try do 2 match_by_head1 per_univ_elem invert_per_univ_elem;
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H);
     simpl_glu_rel;
     try fold (per_univ j m m);
     mauto 4.
diff --git a/theories/Core/Soundness/LogicalRelation/CoreTactics.v b/theories/Core/Soundness/LogicalRelation/CoreTactics.v
index 2b85a547..34bd7691 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreTactics.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreTactics.v
@@ -5,8 +5,7 @@ From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 
 Ltac basic_invert_glu_univ_elem H :=
   progress simp glu_univ_elem in H;
-  inversion H;
-  subst;
+  dependent destruction H;
   try rewrite <- glu_univ_elem_equation_1 in *.
 
 Ltac basic_glu_univ_elem_econstructor :=
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index df1780b4..dd432266 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -405,6 +405,7 @@ Proof.
     assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
     eapply wf_subtyp_refl'.
     mauto 4.
+  - bulky_rewrite.
   - bulky_rewrite.
     mauto 3.
   - destruct_by_head pi_glu_typ_pred.
@@ -916,7 +917,7 @@ Qed.
 Ltac invert_glu_ctx_env H :=
   (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? []]])
-  + (inversion H; subst).
+  + dependent destruction H.
 
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->
diff --git a/theories/Core/Soundness/SubstitutionCases.v b/theories/Core/Soundness/SubstitutionCases.v
index 5fd963f7..8858e558 100644
--- a/theories/Core/Soundness/SubstitutionCases.v
+++ b/theories/Core/Soundness/SubstitutionCases.v
@@ -59,7 +59,7 @@ Proof.
   intros * [SbΓA].
   match_by_head1 glu_ctx_env invert_glu_ctx_env.
   handle_functional_glu_ctx_env.
-  do 2 eexists; repeat split; mauto.
+  do 2 eexists; repeat split; [econstructor | |]; try reflexivity; mauto.
   intros.
   destruct_by_head cons_glu_sub_pred.
   econstructor; mauto.
diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v
index c267ce32..aecd587b 100644
--- a/theories/Extraction/Evaluation.v
+++ b/theories/Extraction/Evaluation.v
@@ -72,7 +72,7 @@ with eval_sub_order : sub -> env -> Prop :=
      eval_sub_order {{{ σ ∘ τ }}} p ).
 
 #[local]
-  Hint Constructors eval_exp_order eval_natrec_order eval_app_order eval_sub_order : mcltt.
+Hint Constructors eval_exp_order eval_natrec_order eval_app_order eval_sub_order : mcltt.
 
 
 Lemma eval_exp_order_sound : forall m p a,
@@ -95,11 +95,11 @@ Proof with (econstructor; intros; functional_eval_rewrite_clear; eauto).
 Qed.
 
 #[export]
-  Hint Resolve eval_exp_order_sound eval_natrec_order_sound eval_app_order_sound eval_sub_order_sound : mcltt.
+Hint Resolve eval_exp_order_sound eval_natrec_order_sound eval_app_order_sound eval_sub_order_sound : mcltt.
 
 
 #[local]
-  Ltac impl_obl_tac1 :=
+Ltac impl_obl_tac1 :=
   match goal with
   | H : eval_exp_order _ _ |- _ => progressive_invert H
   | H : eval_natrec_order _ _ _ _ _ |- _ => progressive_invert H
@@ -108,13 +108,13 @@ Qed.
   end.
 
 #[local]
-  Ltac impl_obl_tac :=
+Ltac impl_obl_tac :=
   repeat impl_obl_tac1; try econstructor; eauto.
 
 Derive Signature for eval_exp_order eval_natrec_order eval_app_order eval_sub_order.
 
-#[tactic="impl_obl_tac"]
-  Equations eval_exp_impl m p (H : eval_exp_order m p) : { d | eval_exp m p d } by struct H :=
+#[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+Equations eval_exp_impl m p (H : eval_exp_order m p) : { d | eval_exp m p d } by struct H :=
 | {{{ Type@i }}}, p, H => exist _ d{{{ 𝕌@i }}} _
 | {{{ #x }}}    , p, H => exist _ (p x) _
 | {{{ ℕ }}}     , p, H => exist _ d{{{ ℕ }}} _
@@ -140,7 +140,7 @@ Derive Signature for eval_exp_order eval_natrec_order eval_app_order eval_sub_or
     let (m, Hm) := eval_exp_impl M p' _ in
     exist _ m _
 
-  with eval_natrec_impl A MZ MS m p (H : eval_natrec_order A MZ MS m p) : { d | eval_natrec A MZ MS m p d } by struct H :=
+with eval_natrec_impl A MZ MS m p (H : eval_natrec_order A MZ MS m p) : { d | eval_natrec A MZ MS m p d } by struct H :=
 | A, MZ, MS, d{{{ zero }}}  , p, H =>
     let (mz, Hmz) := eval_exp_impl MZ p _ in
     exist _ mz _
@@ -153,7 +153,7 @@ Derive Signature for eval_exp_order eval_natrec_order eval_app_order eval_sub_or
     let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ ℕ m }}} _ in
     exist _ d{{{ ⇑ mA (rec m under p return A | zero -> mz | succ -> MS end) }}} _
 
-  with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H :=
+with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H :=
 | d{{{ λ p M }}}        , n, H =>
     let (m, Hm) := eval_exp_impl M d{{{ p ↦ n }}} _ in
     exist _ m _
@@ -161,7 +161,7 @@ Derive Signature for eval_exp_order eval_natrec_order eval_app_order eval_sub_or
     let (b, Hb) := eval_exp_impl B d{{{ p ↦ n }}} _ in
     exist _ d{{{ ⇑ b (m (⇓ a n)) }}} _
 
-  with eval_sub_impl s p (H : eval_sub_order s p) : { p' | eval_sub s p p' } by struct H :=
+with eval_sub_impl s p (H : eval_sub_order s p) : { p' | eval_sub s p p' } by struct H :=
 | {{{ Id }}}, p, H => exist _ p _
 | {{{ Wk }}}, p, H => exist _ d{{{ p↯ }}} _
 | {{{ s ,, M }}}, p, H =>
@@ -173,102 +173,55 @@ Derive Signature for eval_exp_order eval_natrec_order eval_app_order eval_sub_or
     let (p'', Hp'') := eval_sub_impl s p' _ in
     exist _ p'' _.
 
-(* I don't understand why these obligations must be defined separately *)
-(* c.f. https://github.com/mattam82/Coq-Equations/issues/598 *)
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-
 Extraction Inline eval_exp_impl_functional
   eval_natrec_impl_functional
   eval_app_impl_functional
   eval_sub_impl_functional.
 
-
-Ltac edes_rewrite Hind :=
-  let Heq := fresh "Heq" in
-  edestruct Hind as [? Heq];
-  try rewrite Heq in *.
-
-
-Ltac complete_tac :=
-  match goal with
-  | Hind : context[exists _, ?f _ _ = _] |- exists _, (let (_, _) := ?f _ _ in _) = _ =>
-      edes_rewrite Hind
-  | Hind : context[exists _, ?f _ _ _ = _] |- exists _, (let (_, _) := ?f _ _ _ in _) = _ =>
-      edes_rewrite Hind
-  | Hind : context[exists _, ?f _ _ _ _ = _] |- exists _, (let (_, _) := ?f _ _ _ _ in _) = _ =>
-      edes_rewrite Hind
-  | Hind : context[exists _, ?f _ _ _ _ _ = _] |- exists _, (let (_, _) := ?f _ _ _ _ _ in _) = _ =>
-      edes_rewrite Hind
-  | Hind : context[exists _, ?f _ _ _ _ _ _ = _] |- exists _, (let (_, _) := ?f _ _ _ _ _ _ in _) = _ =>
-      edes_rewrite Hind
-  end.
-
-(* The definitions of *_impl already come with soundness proofs, so we only need to prove completeness *)
-
-Lemma eval_exp_impl_complete' : forall M p m,
-    {{ ⟦ M ⟧ p ↘ m }} ->
-    forall (H : eval_exp_order M p),
-    exists H', eval_exp_impl M p H = exist _ m H'
-with eval_natrec_impl_complete' : forall A MZ MS m p r,
-    {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-    forall (H : eval_natrec_order A MZ MS m p),
-    exists H', eval_natrec_impl A MZ MS m p H = exist _ r H'
-with eval_app_impl_complete' : forall m n r,
-    {{ $| m & n |↘ r }} ->
-    forall (H : eval_app_order m n),
-    exists H', eval_app_impl m n H = exist _ r H'
-with eval_sub_impl_complete' : forall σ p p',
-    {{ ⟦ σ ⟧s p ↘ p' }} ->
-    forall (H : eval_sub_order σ p),
-    exists H', eval_sub_impl σ p H = exist _ p' H'.
-Proof with (intros;
-      simp eval_exp_impl;
-      repeat complete_tac;
-      eauto).
-  - clear eval_exp_impl_complete'; induction 1...
-  - clear eval_natrec_impl_complete'; induction 1...
-  - clear eval_app_impl_complete'; induction 1...
-  - clear eval_sub_impl_complete'; induction 1...
-Qed.
+(** The definitions of eval__*_impl already come with soundness proofs,
+    so we only need to prove completeness. However, the completeness
+    is also obvious from the soundness of eval orders and functional
+    nature of eval. *)
 
 #[local]
-  Hint Resolve eval_exp_impl_complete'
-  eval_natrec_impl_complete'
-  eval_app_impl_complete'
-  eval_sub_impl_complete' : mcltt.
+Ltac functional_eval_complete :=
+  lazymatch goal with
+  | |- exists (_ : ?T), _ =>
+      let Horder := fresh "Horder" in
+      assert T as Horder by mauto 3;
+      eexists Horder;
+      lazymatch goal with
+      | |- exists _, ?L = _ =>
+          destruct L;
+          functional_eval_rewrite_clear;
+          eexists; reflexivity
+      end
+  end.
 
 Lemma eval_exp_impl_complete : forall M p m,
     {{ ⟦ M ⟧ p ↘ m }} ->
     exists H H', eval_exp_impl M p H = exist _ m H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_eval_complete.
 Qed.
 
 Lemma eval_natrec_impl_complete : forall A MZ MS m p r,
     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
     exists H H', eval_natrec_impl A MZ MS m p H = exist _ r H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_eval_complete.
 Qed.
 
 Lemma eval_app_impl_complete : forall m n r,
     {{ $| m & n |↘ r }} ->
     exists H H', eval_app_impl m n H = exist _ r H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_eval_complete.
 Qed.
 
 Lemma eval_sub_impl_complete : forall σ p p',
     {{ ⟦ σ ⟧s p ↘ p' }} ->
     exists H H', eval_sub_impl σ p H = exist _ p' H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_eval_complete.
 Qed.
diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v
index fa5ff9f3..3d75800b 100644
--- a/theories/Extraction/NbE.v
+++ b/theories/Extraction/NbE.v
@@ -15,7 +15,7 @@ Inductive initial_env_order : ctx -> Prop :=
      initial_env_order (A :: Γ)).
 
 #[local]
-  Hint Constructors initial_env_order : mcltt.
+Hint Constructors initial_env_order : mcltt.
 
 Lemma initial_env_order_sound : forall Γ p,
     initial_env Γ p ->
@@ -25,24 +25,24 @@ Proof with (econstructor; intros; functional_initial_env_rewrite_clear; function
 Qed.
 
 #[local]
-  Hint Resolve initial_env_order_sound : mcltt.
+Hint Resolve initial_env_order_sound : mcltt.
 
 Derive Signature for initial_env_order.
 
 Section InitialEnvImpl.
 
   #[local]
-    Ltac impl_obl_tac1 :=
+  Ltac impl_obl_tac1 :=
   match goal with
   | H : initial_env_order _ |- _ => progressive_invert H
   end.
 
   #[local]
-    Ltac impl_obl_tac :=
+  Ltac impl_obl_tac :=
     repeat impl_obl_tac1; try econstructor; mauto.
 
-  #[tactic="impl_obl_tac"]
-    Equations initial_env_impl G (H : initial_env_order G) : { p | initial_env G p } by struct H :=
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+  Equations initial_env_impl G (H : initial_env_order G) : { p | initial_env G p } by struct H :=
   | nil, H => exist _ empty_env _
   | cons A G, H =>
       let (p, Hp) := initial_env_impl G _ in
@@ -51,30 +51,41 @@ Section InitialEnvImpl.
 
 End InitialEnvImpl.
 
-
-Lemma initial_env_impl_complete' : forall G p,
-    initial_env G p ->
-    forall (H : initial_env_order G),
-      exists H', initial_env_impl G H = exist _ p H'.
-Proof.
-  induction 1;
-    pose proof eval_exp_impl_complete';
-    intros; simp initial_env_impl;
-    do 2 try complete_tac;
-    eauto.
-Qed.
-
-#[local]
-Hint Resolve initial_env_impl_complete' : mcltt.
-
+(** The definitions of [initial_env_impl] already come with soundness proofs,
+    so we only need to prove completeness. However, the completeness
+    is also obvious from the soundness of eval orders and functional
+    nature of initial_env. *)
 
 Lemma initial_env_impl_complete : forall G p,
     initial_env G p ->
     exists H H', initial_env_impl G H = exist _ p H'.
 Proof.
-  repeat unshelve mauto.
+  intros.
+  assert (Horder : initial_env_order G) by mauto.
+  exists Horder.
+  destruct (initial_env_impl G Horder).
+  functional_initial_env_rewrite_clear.
+  eexists; reflexivity.
 Qed.
 
+(** A similar approach works for nbe implementations.
+    However, as we have 2 implementations (each for [nbe] and [nbe_ty]),
+    We define a tactic to deal with both cases. *)
+
+Ltac functional_nbe_complete :=
+  lazymatch goal with
+  | |- exists (_ : ?T), _ =>
+      let Horder := fresh "Horder" in
+      assert T as Horder by mauto 3;
+      eexists Horder;
+      lazymatch goal with
+      | |- exists _, ?L = _ =>
+          destruct L;
+          functional_nbe_rewrite_clear;
+          eexists; reflexivity
+      end
+  end.
+
 Inductive nbe_order G M A : Prop :=
 | nbe_order_run :
   `( initial_env_order G ->
@@ -90,8 +101,7 @@ Inductive nbe_order G M A : Prop :=
      nbe_order G M A ).
 
 #[local]
-  Hint Constructors nbe_order : mcltt.
-
+Hint Constructors nbe_order : mcltt.
 
 Lemma nbe_order_sound : forall G M A w,
     nbe G M A w ->
@@ -105,22 +115,22 @@ Proof with (econstructor; intros;
 Qed.
 
 #[local]
-  Hint Resolve nbe_order_sound : mcltt.
+Hint Resolve nbe_order_sound : mcltt.
 
 Section NbEDef.
 
   #[local]
-    Ltac impl_obl_tac1 :=
+  Ltac impl_obl_tac1 :=
   match goal with
   | H : nbe_order _ _ _ |- _ => progressive_invert H
   end.
 
   #[local]
-    Ltac impl_obl_tac :=
+  Ltac impl_obl_tac :=
     repeat impl_obl_tac1; try econstructor; mauto.
 
-  #[tactic="impl_obl_tac"]
-    Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+  Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
   | G, M, A, H =>
       let (p, Hp) := initial_env_impl G _ in
       let (a, Ha) := eval_exp_impl A p _ in
@@ -128,33 +138,15 @@ Section NbEDef.
       let (w, Hw) := read_nf_impl (length G) d{{{ ⇓ a m }}} _ in
       exist _ w _.
 
-  Lemma nbe_impl_complete' : forall G M A w,
-      nbe G M A w ->
-      forall (H : nbe_order G M A),
-      exists H', nbe_impl G M A H = exist _ w H'.
-  Proof.
-    induction 1;
-      pose proof initial_env_impl_complete';
-      pose proof eval_exp_impl_complete';
-      pose proof read_nf_impl_complete';
-      intros; simp nbe_impl;
-      repeat complete_tac;
-      eauto.
-  Qed.
-
 End NbEDef.
 
-#[local]
-  Hint Resolve nbe_impl_complete' : mcltt.
-
 Lemma nbe_impl_complete : forall G M A w,
     nbe G M A w ->
-      exists H H', nbe_impl G M A H = exist _ w H'.
+    exists H H', nbe_impl G M A H = exist _ w H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_nbe_complete.
 Qed.
 
-
 Inductive nbe_ty_order G A : Prop :=
 | nbe_ty_order_run :
   `( initial_env_order G ->
@@ -167,8 +159,7 @@ Inductive nbe_ty_order G A : Prop :=
      nbe_ty_order G A ).
 
 #[local]
-  Hint Constructors nbe_ty_order : mcltt.
-
+Hint Constructors nbe_ty_order : mcltt.
 
 Lemma nbe_ty_order_sound : forall G A w,
     nbe_ty G A w ->
@@ -182,22 +173,22 @@ Proof with (econstructor; intros;
 Qed.
 
 #[local]
-  Hint Resolve nbe_ty_order_sound : mcltt.
+Hint Resolve nbe_ty_order_sound : mcltt.
 
 Section NbETyDef.
 
   #[local]
-    Ltac impl_obl_tac1 :=
+  Ltac impl_obl_tac1 :=
   match goal with
   | H : nbe_ty_order _ _ |- _ => progressive_invert H
   end.
 
   #[local]
-    Ltac impl_obl_tac :=
+  Ltac impl_obl_tac :=
     repeat impl_obl_tac1; try econstructor; mauto.
 
-  #[tactic="impl_obl_tac"]
-    Equations nbe_ty_impl G A (H : nbe_ty_order G A) : { w | nbe_ty G A w } by struct H :=
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+  Equations nbe_ty_impl G A (H : nbe_ty_order G A) : { w | nbe_ty G A w } by struct H :=
   | G, A, H =>
       let (p, Hp) := initial_env_impl G _ in
       let (a, Ha) := eval_exp_impl A p _ in
@@ -206,26 +197,9 @@ Section NbETyDef.
 
 End NbETyDef.
 
-Lemma nbe_ty_impl_complete' : forall G A w,
-    nbe_ty G A w ->
-    forall (H : nbe_ty_order G A),
-      exists H', nbe_ty_impl G A H = exist _ w H'.
-Proof.
-  induction 1;
-    pose proof initial_env_impl_complete';
-    pose proof eval_exp_impl_complete';
-    pose proof read_typ_impl_complete';
-    intros; simp nbe_ty_impl;
-    repeat complete_tac;
-    eauto.
-Qed.
-
-#[local]
-  Hint Resolve nbe_ty_impl_complete' : mcltt.
-
 Lemma nbe_ty_impl_complete : forall G A w,
     nbe_ty G A w ->
-      exists H H', nbe_ty_impl G A H = exist _ w H'.
+    exists H H', nbe_ty_impl G A H = exist _ w H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_nbe_complete.
 Qed.
diff --git a/theories/Extraction/PseudoMonadic.v b/theories/Extraction/PseudoMonadic.v
index ea1900c1..7abb5266 100644
--- a/theories/Extraction/PseudoMonadic.v
+++ b/theories/Extraction/PseudoMonadic.v
@@ -1,8 +1,9 @@
 From Coq Require Extraction.
 
-(* We cannot use class based generalization for
-   the following definitions as Coq does not support
-   polymorphism across [Prop] and [Set] *)
+(** We cannot use class based generalization for
+    the following definitions as Coq does not support
+    extractable polymorphism across [Prop] and [Set].
+    #See <a href="https://github.com/coq/coq/issues/19452">this Coq issue</a># *)
 
 Definition sumbool_failable_bind {A B} (ab : {A} + {B}) {C D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
   match ab with
diff --git a/theories/Extraction/Readback.v b/theories/Extraction/Readback.v
index 1f990b43..9eb7bcde 100644
--- a/theories/Extraction/Readback.v
+++ b/theories/Extraction/Readback.v
@@ -76,8 +76,7 @@ with read_typ_order : nat -> domain -> Prop :=
     read_typ_order s d{{{ ⇑ a b }}} ).
 
 #[local]
-  Hint Constructors read_nf_order read_ne_order read_typ_order : mcltt.
-
+Hint Constructors read_nf_order read_ne_order read_typ_order : mcltt.
 
 Lemma read_nf_order_sound : forall s d m,
     {{ Rnf d in s ↘ m }} ->
@@ -95,13 +94,12 @@ Proof with (econstructor; intros; functional_eval_rewrite_clear; mauto).
 Qed.
 
 #[export]
-  Hint Resolve read_nf_order_sound read_ne_order_sound read_typ_order_sound : mcltt.
+Hint Resolve read_nf_order_sound read_ne_order_sound read_typ_order_sound : mcltt.
 
 Derive Signature for read_nf_order read_ne_order read_typ_order.
 
-
 #[local]
-  Ltac impl_obl_tac1 :=
+Ltac impl_obl_tac1 :=
   match goal with
   | H : read_nf_order _ _ |- _ => progressive_invert H
   | H : read_ne_order _ _ |- _ => progressive_invert H
@@ -109,10 +107,10 @@ Derive Signature for read_nf_order read_ne_order read_typ_order.
   end.
 
 #[local]
-  Ltac impl_obl_tac :=
+Ltac impl_obl_tac :=
   repeat impl_obl_tac1; try econstructor; mauto.
 
-#[tactic="impl_obl_tac"]
+#[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
 Equations read_nf_impl s d (H : read_nf_order s d) : { m | {{ Rnf d in s ↘ m }} } by struct H :=
 | s, d{{{ ⇓ 𝕌@i a }}}      , H =>
     let (A, HA) := read_typ_impl s a _ in
@@ -163,69 +161,47 @@ Equations read_nf_impl s d (H : read_nf_order s d) : { m | {{ Rnf d in s ↘ m }
     let (B, HB) := read_ne_impl s b _ in
     exist _ n{{{ ⇑ B }}} _.
 
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-Next Obligation. impl_obl_tac. Defined.
-
 Extraction Inline read_nf_impl_functional
   read_ne_impl_functional
   read_typ_impl_functional.
 
-#[local]
-  Ltac pose_other_lemmas :=
-  pose proof eval_exp_impl_complete';
-  pose proof eval_natrec_impl_complete';
-  pose proof eval_app_impl_complete';
-  pose proof eval_sub_impl_complete'.
-
-Lemma read_nf_impl_complete' : forall s d m,
-    {{ Rnf d in s ↘ m }} ->
-    forall (H : read_nf_order s d),
-      exists H', read_nf_impl s d H = exist _ m H'
-with read_ne_impl_complete' : forall s d m,
-    {{ Rne d in s ↘ m }} ->
-    forall (H : read_ne_order s d),
-      exists H', read_ne_impl s d H = exist _ m H'
-with read_typ_impl_complete' : forall s d m,
-    {{ Rtyp d in s ↘ m }} ->
-    forall (H : read_typ_order s d),
-      exists H', read_typ_impl s d H = exist _ m H'.
-Proof with (pose_other_lemmas;  (* so that complete_tac uses these lemmas *)
-            intros;
-            simp read_nf_impl;
-            repeat complete_tac;
-            eauto).
-  - clear read_nf_impl_complete'; induction 1...
-  - clear read_ne_impl_complete'; induction 1...
-  - clear read_typ_impl_complete'; induction 1...
-Qed.
+(** The definitions of read__*_impl already come with soundness proofs,
+    so we only need to prove completeness. However, the completeness
+    is also obvious from the soundness of eval orders and functional
+    nature of readback. *)
 
 #[local]
-  Hint Resolve read_nf_impl_complete'
-  read_ne_impl_complete'
-  read_typ_impl_complete' : mcltt.
+Ltac functional_read_complete :=
+  lazymatch goal with
+  | |- exists (_ : ?T), _ =>
+      let Horder := fresh "Horder" in
+      assert T as Horder by mauto 3;
+      eexists Horder;
+      lazymatch goal with
+      | |- exists _, ?L = _ =>
+          destruct L;
+          functional_read_rewrite_clear;
+          eexists; reflexivity
+      end
+  end.
 
 Lemma read_nf_impl_complete : forall s d m,
     {{ Rnf d in s ↘ m }} ->
     exists H H', read_nf_impl s d H = exist _ m H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_read_complete.
 Qed.
 
 Lemma read_ne_impl_complete : forall s d m,
     {{ Rne d in s ↘ m }} ->
     exists H H', read_ne_impl s d H = exist _ m H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_read_complete.
 Qed.
 
 Lemma read_typ_impl_complete : forall s d m,
     {{ Rtyp d in s ↘ m }} ->
     exists H H', read_typ_impl s d H = exist _ m H'.
 Proof.
-  repeat unshelve mauto.
+  intros; functional_read_complete.
 Qed.
diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index b7c585ad..48fc5de7 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -21,7 +21,7 @@ Ltac subtyping_tac :=
       try congruence
   end.
 
-#[tactic="subtyping_tac"]
+#[tactic="subtyping_tac",derive(equations=no,eliminator=no)]
 Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
 | n{{{ Type@i }}}, n{{{ Type@j }}} =>
     let*b _ := Compare_dec.le_lt_dec i j while _ in
@@ -36,6 +36,10 @@ Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆
   | left _ => left _
   | right _ => right _
   }.
+
+(** The definitions of [subtyping_nf_impl] already come with soundness proofs,
+    as well as obvious completeness. *)
+
 Theorem subtyping_nf_impl_complete : forall A B,
     {{ ⊢anf A ⊆ B }} ->
     exists H, subtyping_nf_impl A B = left H.
@@ -71,7 +75,7 @@ Ltac subtyping_impl_tac1 :=
 Ltac subtyping_impl_tac :=
   repeat subtyping_impl_tac1; try econstructor; mauto.
 
-#[tactic="subtyping_impl_tac"]
+#[tactic="subtyping_impl_tac",derive(equations=no,eliminator=no)]
 Equations subtyping_impl G A B (H : subtyping_order G A B) :
   { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
 | G, A, B, H =>
@@ -85,6 +89,8 @@ Next Obligation.
   contradiction.
 Qed.
 
+(** Similar for [subtyping_impl]. *)
+
 Theorem subtyping_impl_complete' : forall G A B,
     {{G ⊢a A ⊆ B}} ->
     forall (H : subtyping_order G A B),
diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
index cec25457..c203851c 100644
--- a/theories/Extraction/TypeCheck.v
+++ b/theories/Extraction/TypeCheck.v
@@ -45,12 +45,15 @@ Section lookup.
 End lookup.
 
 Section type_check.
+  #[derive(equations=no,eliminator=no)]
   Equations get_level_of_type_nf (A : nf) : { i | A = n{{{ Type@i }}} } + { forall i, A <> n{{{ Type@i }}} } :=
   | n{{{ Type@i }}} => pureo (exist _ i _)
   | _               => inright _
   .
 
-  (* Don't forget to use 9th bit of [Extraction Flag] (for example, [Set Extraction Flag 1007.]) *)
+  (** Don't forget to use 9th bit of [Extraction Flag] (for example, [Set Extraction Flag 1007.]).
+      Otherwise, this function would introduce redundant pair construction/pattern matching. *)
+  #[derive(equations=no,eliminator=no)]
   Equations get_subterms_of_pi_nf (A : nf) : { B & { C | A = n{{{ Π B C }}} } } + { forall B C, A <> n{{{ Π B C }}} } :=
   | n{{{ Π B C }}} => pureo (existT _ B (exist _ C _))
   | _              => inright _
@@ -336,8 +339,48 @@ Section type_check.
   Qed.
 
   Extraction Inline type_check_functional type_infer_functional.
+
+  Lemma type_infer_order_soundness : forall G M A,
+      {{ G ⊢a M ⟹ A }} ->
+      type_infer_order M
+  with type_check_order_soundness : forall G M A,
+      {{ G ⊢a M ⟸ A }} ->
+      type_check_order M.
+  Proof.
+    - clear type_infer_order_soundness.
+      induction 1; mauto 3.
+      econstructor; mauto 3.
+    - clear type_check_order_soundness.
+      induction 1; mauto 3.
+  Qed.
 End type_check.
 
+#[local]
+Hint Resolve type_check_order_soundness type_infer_order_soundness : mcltt.
+
+Lemma type_check_complete' : forall G M A (HA : exists i, {{ G ⊢ A : Type@i }}),
+    {{ G ⊢a M ⟸ A }} ->
+    exists H H', type_check G A HA M H = left H'.
+Proof.
+  intros ? ? ? [] ?.
+  assert (Horder : type_check_order M) by mauto.
+  exists Horder.
+  dec_complete.
+Qed.
+
+Lemma type_infer_complete : forall G M A (HG : {{ ⊢ G }}),
+    {{ G ⊢a M ⟹ A }} ->
+    exists H H', type_infer G HG M H = inleft (exist _ A H').
+Proof.
+  intros.
+  assert (Horder : type_infer_order M) by mauto.
+  exists Horder.
+  destruct (type_infer G HG M Horder) as [[? []] |].
+  - functional_alg_type_infer_rewrite_clear.
+    eexists; reflexivity.
+  - contradict H; intuition.
+Qed.
+
 Section type_check_closed.
   #[local]
   Ltac impl_obl_tac :=
@@ -378,3 +421,8 @@ Section type_check_closed.
     mauto 3 using alg_type_check_sound.
   Qed.
 End type_check_closed.
+
+Lemma type_check_closed_complete : forall A (HA : user_exp A) M (HM : user_exp M),
+    {{ ⋅ ⊢ M : A }} ->
+    exists H', type_check_closed A HA M HM = left H'.
+Proof. intros; dec_complete. Qed.
diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages
index d3002c11..2599b992 100644
--- a/theories/Frontend/parserMessages.messages
+++ b/theories/Frontend/parserMessages.messages
@@ -461,4 +461,4 @@ prog: INT COLON RPAREN
 ##
 
 An expression is expected.
-This token is invalid for the beginning of an expression.
\ No newline at end of file
+This token is invalid for the beginning of an expression.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index af0b538d..4944dbf2 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -229,22 +229,16 @@ Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow.
 (* Improve type class resolution *)
 
 #[export]
-  Hint Extern 1 => eassumption : typeclass_instances.
-
-Ltac predicate_resolve :=
-  lazymatch goal with
-  | |- @Reflexive _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Reflexive
-  | |- @Symmetric _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Symmetric
-  | |- @Transitive _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Transitive
-  | |- @Transitive _ (@predicate_implication _) =>
-      simple apply @PreOrder_Transitive
-  end.
+Hint Extern 1 => eassumption : typeclass_instances.
 
 #[export]
-Hint Extern 1 => predicate_resolve : typeclass_instances.
+Hint Extern 1 (@Reflexive _ (@predicate_equivalence _)) => simple apply @Equivalence_Reflexive : typeclass_instances.
+#[export]
+Hint Extern 1 (@Symmetric _ (@predicate_equivalence _)) => simple apply @Equivalence_Symmetric : typeclass_instances.
+#[export]
+Hint Extern 1 (@Transitive _ (@predicate_equivalence _)) => simple apply @Equivalence_Transitive : typeclass_instances.
+#[export]
+Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrder_Transitive : typeclass_instances.
 
 
 (* intuition tactic default setting *)