diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v
index 01ee2441..c224cef6 100644
--- a/theories/Extraction/NbE.v
+++ b/theories/Extraction/NbE.v
@@ -65,7 +65,7 @@ Proof.
 Qed.
 
 #[local]
-  Hint Resolve initial_env_impl_complete' : mcltt.
+Hint Resolve initial_env_impl_complete' : mcltt.
 
 
 Lemma initial_env_impl_complete : forall G p,
diff --git a/theories/Extraction/PseudoMonadic.v b/theories/Extraction/PseudoMonadic.v
new file mode 100644
index 00000000..ea1900c1
--- /dev/null
+++ b/theories/Extraction/PseudoMonadic.v
@@ -0,0 +1,49 @@
+From Coq Require Extraction.
+
+(* We cannot use class based generalization for
+   the following definitions as Coq does not support
+   polymorphism across [Prop] and [Set] *)
+
+Definition sumbool_failable_bind {A B} (ab : {A} + {B}) {C D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
+  match ab with
+  | left a => next a
+  | right b => right (fail b)
+  end.
+Transparent sumbool_failable_bind.
+Arguments sumbool_failable_bind /.
+
+Notation "'let*b' a ':=' ab 'while' fail 'in' next" := (sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Notation "'pureb' a" := (left a) (at level 0, only parsing).
+
+Definition sumor_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
+  match ab with
+  | inleft a => next a
+  | inright b => inright (fail b)
+  end.
+Transparent sumor_failable_bind.
+Arguments sumor_failable_bind /.
+
+Notation "'let*o' a ':=' ab 'while' fail 'in' next" := (sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Notation "'pureo' a" := (inleft a) (at level 0, only parsing).
+
+Definition sumbool_sumor_failable_bind {A B} (ab : {A} + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
+  match ab with
+  | left a => next a
+  | right b => inright (fail b)
+  end.
+Transparent sumbool_sumor_failable_bind.
+Arguments sumbool_sumor_failable_bind /.
+
+Notation "'let*b->o' a ':=' ab 'while' fail 'in' next" := (sumbool_sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+
+Definition sumor_sumbool_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
+  match ab with
+  | inleft a => next a
+  | inright b => right (fail b)
+  end.
+Transparent sumor_sumbool_failable_bind.
+Arguments sumor_sumbool_failable_bind /.
+
+Notation "'let*o->b' a ':=' ab 'while' fail 'in' next" := (sumor_sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+
+Extraction Inline sumbool_failable_bind sumor_failable_bind sumbool_sumor_failable_bind sumor_sumbool_failable_bind.
diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index c99e48d1..b7c585ad 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -1,13 +1,13 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Algorithmic Require Import Subtyping.Definitions.
 From Mcltt.Core Require Import NbE.
-From Mcltt.Extraction Require Import Evaluation NbE.
+From Mcltt.Extraction Require Import Evaluation NbE PseudoMonadic.
 From Equations Require Import Equations.
 Import Domain_Notations.
 
-
 #[local]
-  Ltac subtyping_tac :=
+Ltac subtyping_tac :=
+  intros;
   lazymatch goal with
   | |- {{ ⊢anf ~_ ⊆ ~_ }} =>
       subst;
@@ -23,22 +23,19 @@ Import Domain_Notations.
 
 #[tactic="subtyping_tac"]
 Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
-| n{{{ Type@i }}}, n{{{ Type@j }}} with Compare_dec.le_lt_dec i j => {
-  | left _ => left _;
-  | right _ => right _
-  }
-| n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
-  | left _ with subtyping_nf_impl B B' => {
-    | left _ => left _
-    | right _ => right _
-    }
-  | right _ => right _
-  }
+| n{{{ Type@i }}}, n{{{ Type@j }}} =>
+    let*b _ := Compare_dec.le_lt_dec i j while _ in
+    pureb _
+| n{{{ Π A B }}}, n{{{ Π A' B' }}} =>
+    let*b _ := nf_eq_dec A A' while _ in
+    let*b _ := subtyping_nf_impl B B' while _ in
+    pureb _
+(* Pseudo-monadic syntax for the next catch-all branch
+   generates some unsolved obligations *)
 | A, B with nf_eq_dec A B => {
   | left _ => left _
   | right _ => right _
   }.
-
 Theorem subtyping_nf_impl_complete : forall A B,
     {{ ⊢anf A ⊆ B }} ->
     exists H, subtyping_nf_impl A B = left H.
@@ -46,15 +43,13 @@ Proof.
   intros; dec_complete.
 Qed.
 
-
 Inductive subtyping_order G A B :=
 | subtyping_order_run :
   nbe_ty_order G A ->
   nbe_ty_order G B ->
   subtyping_order G A B.
 #[local]
-  Hint Constructors subtyping_order : mcltt.
-
+Hint Constructors subtyping_order : mcltt.
 
 Lemma subtyping_order_sound : forall G A B,
     {{ G ⊢a A ⊆ B }} ->
@@ -66,34 +61,30 @@ Proof.
 Qed.
 
 #[local]
-  Ltac subtyping_impl_tac1 :=
+Ltac subtyping_impl_tac1 :=
   match goal with
   | H : subtyping_order _ _ _ |- _ => progressive_invert H
   | H : nbe_ty_order _ _ |- _ => progressive_invert H
   end.
 
 #[local]
-  Ltac subtyping_impl_tac :=
+Ltac subtyping_impl_tac :=
   repeat subtyping_impl_tac1; try econstructor; mauto.
 
-
 #[tactic="subtyping_impl_tac"]
 Equations subtyping_impl G A B (H : subtyping_order G A B) :
   { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
 | G, A, B, H =>
     let (a, Ha) := nbe_ty_impl G A _ in
     let (b, Hb) := nbe_ty_impl G B _ in
-    match subtyping_nf_impl a b with
-    | left _ => left _
-    | right _ => right _
-    end.
+    let*b _ := subtyping_nf_impl a b while _ in
+    pureb _.
 Next Obligation.
   progressive_inversion.
   functional_nbe_rewrite_clear.
   contradiction.
 Qed.
 
-
 Theorem subtyping_impl_complete' : forall G A B,
     {{G ⊢a A ⊆ B}} ->
     forall (H : subtyping_order G A B),
@@ -103,7 +94,7 @@ Proof.
 Qed.
 
 #[local]
- Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
+Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
 
 Theorem subtyping_impl_complete : forall G A B,
     {{G ⊢a A ⊆ B}} ->
diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
index a134ad23..317e840c 100644
--- a/theories/Extraction/TypeCheck.v
+++ b/theories/Extraction/TypeCheck.v
@@ -1,104 +1,381 @@
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness NbE Soundness SystemOpt.
-From Mcltt.Extraction Require Import NbE.
+From Mcltt.Algorithmic Require Import Typing.Definitions Typing.Lemmas.
+From Mcltt.Core Require Import
+  Completeness
+  Completeness.Consequences.Inversions
+  Completeness.Consequences.Types
+  Completeness.FundamentalTheorem
+  Completeness.LogicalRelation
+  NbE
+  Semantic.Consequences
+  Semantic.Realizability
+  Soundness
+  SystemOpt.
+From Mcltt.Extraction Require Import NbE PseudoMonadic Subtyping.
+From Mcltt.Frontend Require Import Elaborator.
 From Equations Require Import Equations.
 Import Domain_Notations.
 
-(* Section nf_subsumption_dec. *)
-(*   #[local] *)
-(*   Ltac impl_obl_tac := *)
-(*     match goal with *)
-(*     | |- nf_subsumption _ _ => mauto 2 *)
-(*     | A := _ : nf |- ~ (nf_subsumption _ _) => *)
-(*         let H := fresh "H" in *)
-(*         subst A; intro H; dependent destruction H; congruence *)
-(*     | |- ~ (nf_subsumption _ _) => *)
-(*         let H := fresh "H" in *)
-(*         intro H; dependent destruction H; lia *)
-(*     end. *)
-
-(*   #[tactic=impl_obl_tac] *)
-(*   Equations nf_subsumption_dec A A' : {nf_subsumption A A'} + {~ nf_subsumption A A'} := *)
-(*   | n{{{ Type@i }}}, n{{{ Type@j }}} => *)
-(*       match Compare_dec.le_lt_dec i j with *)
-(*       | left _ => left _ *)
-(*       | right _ => right _ *)
-(*       end *)
-(*   (* Here we have a separate clause for n{{{ Type@i }}} so that we can extract a more efficient code *) *)
-(*   | n{{{ Type@i }}}, _ => right _ *)
-(*   | A, A' => *)
-(*       match nf_eq_dec A A' with *)
-(*       | left _ => left _ *)
-(*       | right _ => right _ *)
-(*       end. *)
-(* End nf_subsumption_dec. *)
-
-(* Section conversion_dec. *)
-(*   #[local] *)
-(*   Ltac impl_obl_tac := *)
-(*     match goal with *)
-(*     | |- nbe_order ?G ?M ?A => *)
-(*         (on_all_hyp: fun H => apply soundness in H); *)
-(*         destruct_conjs; *)
-(*         eapply nbe_order_sound; eassumption *)
-(*     | |- False => *)
-(*         (on_all_hyp: fun H => apply completeness in H); *)
-(*         destruct_conjs; *)
-(*         functional_nbe_rewrite_clear; *)
-(*         congruence *)
-(*     | _ => *)
-(*         (on_all_hyp: fun H => apply soundness in H); *)
-(*         destruct_conjs; *)
-(*         functional_nbe_rewrite_clear; *)
-(*         mauto *)
-(*     end. *)
-
-(*   #[tactic="impl_obl_tac"] *)
-(*   Equations conversion_dec G A M (HM : {{ G ⊢ M : A }}) M' (HM' : {{ G ⊢ M' : A }}) : { {{ G ⊢ M ≈ M' : A }} } + { ~ {{ G ⊢ M ≈ M' : A }} } := *)
-(*   | G, A, M, HM, M', HM' => *)
-(*       let (W, HW) := nbe_impl G M A _ in *)
-(*       let (W', HW') := nbe_impl G M' A _ in *)
-(*       match nf_eq_dec W W' with *)
-(*       | left _ => left _ *)
-(*       | right _ => right _ *)
-(*       end. *)
-(*   Next Obligation. impl_obl_tac. Qed. *)
-(* End conversion_dec. *)
-
-(* Section typ_subsumption_dec. *)
-(*   #[local] *)
-(*   Ltac impl_obl_tac := *)
-(*     match goal with *)
-(*     | |- nbe_order ?G ?M ?A => *)
-(*         (on_all_hyp: fun H => apply soundness in H); *)
-(*         destruct_conjs; *)
-(*         eapply nbe_order_sound; eassumption *)
-(*     | H: nbe ?G ?A {{{ Type@?i }}} ?W, H': nbe ?G ?A' {{{ Type@?i' }}} ?W' |- {{ ~?G ⊢ ~?A ⊆ ~?A' }} => *)
-(*         (on_all_hyp: fun H => apply soundness in H); *)
-(*         destruct_conjs; *)
-(*         functional_nbe_rewrite_clear; *)
-(*         rename HA into W; *)
-(*         rename HA' into W'; *)
-(*         assert {{ G ⊢ W : Type@i }} by (gen_presups; eassumption); *)
-(*         assert {{ G ⊢ W' : Type@i }} by (gen_presups; eassumption); *)
-(*         assert {{ G ⊢ W ⊆ W' }} by mauto; *)
-(*         etransitivity; *)
-(*         mauto *)
-(*     | H: ~ (nf_subsumption ?W ?W') |- ~ {{ ~?G ⊢ ~?A ⊆ ~?A' }} => *)
-(*         contradict H; *)
-(*         apply completeness_for_typ_subsumption in H; *)
-(*         destruct_conjs; *)
-(*         functional_nbe_rewrite_clear; *)
-(*         eassumption *)
-(*     end. *)
-
-(*   #[tactic="impl_obl_tac"] *)
-(*   Equations typ_subsumption_dec G i A (HA : {{ G ⊢ A : Type@i }}) A' (HA' : {{ G ⊢ A' : Type@i }}) : { {{ G ⊢ A ⊆ A' }} } + { ~ {{ G ⊢ A ⊆ A' }} } := *)
-(*   | G, i, A, HA, A', HA' => *)
-(*       let (W, HW) := nbe_impl G A {{{ Type@i }}} _ in *)
-(*       let (W', HW') := nbe_impl G A' {{{ Type@i }}} _ in *)
-(*       match nf_subsumption_dec W W' with *)
-(*       | left _ => left _ *)
-(*       | right _ => right _ *)
-(*       end. *)
-(* End typ_subsumption_dec. *)
+Section lookup.
+  #[local]
+  Ltac impl_obl_tac1 :=
+    match goal with
+    | |- ~_ => intro
+    | H: {{ ⊢ ~_, ~_ }} |- _ => inversion_clear H
+    | H: {{ # _ : ~_ ∈ ⋅ }} |- _ => inversion_clear H
+    | H: {{ # (S _) : ~_ ∈ ~_, ~_ }} |- _ => inversion_clear H
+    end.
+
+  #[local]
+  Ltac impl_obl_tac :=
+    intros;
+    repeat impl_obl_tac1;
+    intuition (mauto 4).
+
+  #[tactic="impl_obl_tac"]
+  Equations lookup G (HG : {{ ⊢ G }}) x : { A | {{ #x : A ∈ G }} } + { forall A, ~ {{ #x : A ∈ G }} } :=
+  | {{{ G, A }}}, HG, x with x => {
+    | 0 => pureo (exist _ {{{ A[Wk] }}} _)
+    | S x' =>
+        let*o (exist _ B _) := lookup G _ x' while _ in
+        pureo (exist _ {{{ B[Wk] }}} _)
+    }
+  | {{{ ⋅ }}}, HG, x => inright _.
+End lookup.
+
+Section type_check.
+  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 _
+  .
+
+  Extraction Inline get_level_of_type_nf.
+
+  Inductive type_check_order : exp -> Prop :=
+  | tc_ti : forall {A}, type_infer_order A -> type_check_order A
+  with type_infer_order : exp -> Prop :=
+  | ti_typ : forall {i}, type_infer_order {{{ Type@i }}}
+  | ti_nat : type_infer_order {{{ ℕ }}}
+  | ti_zero : type_infer_order {{{ zero }}}
+  | ti_succ : forall {M}, type_check_order M -> type_infer_order {{{ succ M }}}
+  | ti_natrec : forall {A MZ MS M}, type_check_order M -> type_infer_order A -> type_check_order MZ -> type_check_order MS -> type_infer_order {{{ rec M return A | zero -> MZ | succ -> MS end }}}
+  | ti_pi : forall {A B}, type_infer_order {{{ A }}} -> type_infer_order {{{ B }}} -> type_infer_order {{{ Π A B }}}
+  | ti_fn : forall {A M}, type_infer_order A -> type_infer_order M -> type_infer_order {{{ λ A M }}}
+  | ti_app : forall {M N}, type_infer_order M -> type_check_order N -> type_infer_order {{{ M N }}}
+  | ti_vlookup : forall {x}, type_infer_order {{{ #x }}}
+  .
+
+  #[local]
+  Hint Constructors type_check_order type_infer_order : mcltt.
+
+  Lemma user_exp_to_type_infer_order : forall M,
+      user_exp M ->
+      type_infer_order M.
+  Proof.
+    intros M HM.
+    enough (type_check_order M) as [] by eassumption.
+    induction HM; progressive_inversion; mauto 3.
+  Qed.
+
+  #[local]
+  Ltac clear_defs :=
+    repeat lazymatch goal with
+      | H: (forall (G : ctx) (A : typ),
+               (exists i : nat, {{ G ⊢ A : Type@i }}) ->
+               forall M : typ,
+                 type_check_order M ->
+                 ({ {{ G ⊢a M ⟸ A }} } + { ~ {{ G ⊢a M ⟸ A }} }))
+        |- _ =>
+          clear H
+      | H: (let H := fixproto in
+            forall (G : ctx) (A : typ),
+              (exists i : nat, {{ G ⊢ A : Type @ i }}) -> forall M : typ, type_check_order M -> { {{ G ⊢a M ⟸ A }} } + { ~ {{ G ⊢a M ⟸ A }} })
+        |- _ =>
+          clear H
+      | H: (let H := fixproto in
+            forall G : ctx,
+              {{ ⊢ G }} ->
+              forall M : typ,
+                type_infer_order M ->
+                ({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i : nat, {{ G ⊢a ~(nf_to_exp B) ⟹ Type@i }}) } + { forall C : nf, ~ {{ G ⊢a M ⟹ C }} }))
+        |- _ =>
+          clear H
+      | H: (forall G : ctx,
+               {{ ⊢ G }} ->
+               forall M : typ,
+                 type_infer_order M ->
+                 ({ B : nf | {{ G ⊢a M ⟹ B }} /\ (exists i : nat, {{ G ⊢a ~(nf_to_exp B) ⟹ Type@i }}) } + { forall C : nf, ~ {{ G ⊢a M ⟹ C }} }))
+        |- _ =>
+          clear H
+    end.
+
+  #[local]
+  Ltac impl_obl_tac_helper :=
+    match goal with
+    | H: type_infer_order _ |- _ => progressive_invert H
+    end.
+
+  #[local]
+  Ltac impl_obl_tac :=
+    clear_defs;
+    repeat impl_obl_tac_helper;
+    destruct_conjs;
+    match goal with
+    | |- {{ ⊢ ~_ }} => gen_presups; mautosolve 4
+    | H: {{ ~?G ⊢ ~?A : Type@?i }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_left; mautosolve 4
+    | H: {{ ~?G ⊢ ~?A : Type@?j }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_right; mautosolve 4
+    | |- {{ ~_ ⊢ ~_ : ~_ }} => gen_presups; mautosolve 4
+    | |- (~ {{ ~_ ⊢a ~_ ⊆ ~_ }} -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) =>
+        let H := fresh "H" in
+        intros ? H;
+        inversion H;
+        functional_alg_type_infer_rewrite_clear;
+        firstorder
+    | |- ((forall A : nf, ~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) =>
+        let H := fresh "H" in
+        intros ? H;
+        inversion H;
+        firstorder
+    | |- type_infer_order _ => eassumption; fail 1
+    | |- type_check_order _ => eassumption; fail 1
+    | |- subtyping_order ?G ?A ?B =>
+        enough (exists i, {{ G ⊢ A : ~n{{{ Type@i }}} }}) as [? [? []]%soundness_ty];
+        only 1: enough (exists j, {{ G ⊢ B : ~n{{{ Type@j }}} }}) as [? [? []]%soundness_ty];
+        only 1: solve [econstructor; eauto 3 using nbe_ty_order_sound];
+        solve [mauto 4 using alg_type_infer_sound]
+    | _ =>
+        unfold not;
+        intros;
+        progressive_inversion;
+        functional_alg_type_infer_rewrite_clear;
+        solve [congruence | mautosolve 3]
+    | _ => idtac
+    end.
+
+  Definition inspect {A : Set} (a : A) : { b : A | a = b } := (exist _ a eq_refl).
+
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+  Equations type_check G A (HA : (exists i, {{ G ⊢ A : Type@i }})) M (H : type_check_order M) : { {{ G ⊢a M ⟸ A }} } + { ~ {{ G ⊢a M ⟸ A }} } by struct H :=
+  | G, A, HA, M, H =>
+      let*o->b (exist _ B _) := type_infer G _ M _ while _ in
+      let*b _ := subtyping_impl G B A _ while _ in
+      pureb _
+  with type_infer G (HG : {{ ⊢ G }}) M (H : type_infer_order M) : { A : nf | {{ G ⊢a M ⟹ A }} /\ (exists i, {{ G ⊢a A ⟹ Type@i }}) } + { forall A, ~ {{ G ⊢a M ⟹ A }} } by struct H :=
+  | G, HG, M, H with M => {
+    | {{{ Type@j }}} =>
+        pureo (exist _ n{{{ Type@(S j) }}} _)
+    | {{{ ℕ }}} => 
+        pureo (exist _ n{{{ Type@0 }}} _)
+    | {{{ zero }}} =>
+        pureo (exist _ n{{{ ℕ }}} _)
+    | {{{ succ M' }}} =>
+        let*b->o _ := type_check G {{{ ℕ }}} _ M' _ while _ in
+        pureo (exist _ n{{{ ℕ }}} _)
+    | {{{ rec M' return A' | zero -> MZ | succ -> MS end }}} =>
+        let*b->o _ := type_check G {{{ ℕ }}} _ M' _ while _ in
+        let*o (exist _ UA' _) := type_infer {{{ G, ℕ }}} _ A' _ while _ in
+        let*o (exist _ i _) :=  get_level_of_type_nf UA' while _ in
+        let*b->o _ := type_check G {{{ A'[Id,,zero] }}} _ MZ _ while _ in
+        let*b->o _ := type_check {{{ G, ℕ, A' }}} {{{ A'[Wk∘Wk,,succ #1] }}} _ MS _ while _ in
+        let (A'', _) := nbe_ty_impl G {{{ A'[Id,,M'] }}} _ in
+        pureo (exist _ A'' _)
+    | {{{ Π B C }}} =>
+        let*o (exist _ UB _) := type_infer G _ B _ while _ in
+        let*o (exist _ i _) :=  get_level_of_type_nf UB while _ in
+        let*o (exist _ UC _) := type_infer {{{ G, B }}} _ C _ while _ in
+        let*o (exist _ j _) :=  get_level_of_type_nf UC while _ in
+        pureo (exist _ n{{{ Type@(max i j) }}} _)
+    | {{{ λ A' M' }}} =>
+        let*o (exist _ UA' _) := type_infer G _ A' _ while _ in
+        let*o (exist _ i _) :=  get_level_of_type_nf UA' while _ in
+        let*o (exist _ B' _) := type_infer {{{ G, A' }}} _ M' _ while _ in
+        let (A'', _) := nbe_ty_impl G A' _ in
+        pureo (exist _ n{{{ Π A'' B' }}} _)
+    | {{{ M' N' }}} with type_infer G _ M' _ => {
+      | inleft (exist _ (nf_pi A B) _) =>
+          let*b->o _ := type_check G A _ N' _ while _ in
+          let (B', _) := nbe_ty_impl G {{{ B[Id,,N'] }}} _ in
+          pureo (exist _ B' _)
+      | _ => inright _
+      }
+    | {{{ #x }}} =>
+        let*o (exist _ A _) := lookup G _ x while _ in
+        let (A', _) := nbe_ty_impl G A _ in
+        pureo (exist _ A' _)
+    | _ => inright _
+    }
+  .
+
+  Next Obligation (* {{ G ⊢a succ M' ⟹ ℕ }} /\ (exists i, {{ G ⊢a ℕ ⟹ Type@i }}) *).
+    clear_defs.
+    mautosolve 4.
+  Qed.
+  
+  Next Obligation (* exists j, {{ G ⊢ A'[Id,,zero] : Type@j }} *).
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    eexists.
+    assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
+  Qed.
+
+  Next Obligation (* exists j, {{ G, ℕ, A' ⊢ A'[Wk∘Wk,,succ #1] : Type@i }} *).
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    eexists.
+    assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
+  Qed.
+
+  Next Obligation (* nbe_ty_order G {{{ A'[Id,,M'] }}} *).
+    clear_defs.
+    enough (exists i, {{ G ⊢ A'[Id,,M'] : ~n{{{ Type@i }}} }}) as [? [? []]%exp_eq_refl%completeness_ty]
+        by eauto 3 using nbe_ty_order_sound.
+    eexists.
+    assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ ℕ : Type@0 }} by mauto 3.
+    mauto 4 using alg_type_check_sound.
+  Qed.
+
+  Next Obligation (* {{ G ⊢a rec M' return A' | zero -> MZ | succ -> MS end ⟹ A'' }} /\ (exists j, {{ G ⊢a A'' ⟹ Type@j }}) *).
+    clear_defs.
+    split; [mauto 3 |].
+    assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ ℕ : Type@0 }} by mauto 3.
+    assert {{ G ⊢ A'[Id,,M'] ≈ A'' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert (user_exp A'') by trivial using user_exp_nf.
+    assert (exists j, {{ G ⊢a A'' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 3); firstorder.
+  Qed.
+
+  Next Obligation (* nbe_ty_order G A *).
+    clear_defs.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [? [? []]%soundness_ty] by mauto 3.
+    mauto 3 using nbe_ty_order_sound.
+  Qed.
+
+  Next Obligation. (* {{ G ⊢a #x ⟹ A' }} /\ (exists i, {{ G ⊢a A' ⟹ Type@i }}) *)
+    clear_defs.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [i] by mauto 3.
+    assert {{ G ⊢ A ≈ A' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert (user_exp A') by trivial using user_exp_nf.
+    assert (exists j, {{ G ⊢a A' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 4); firstorder mauto 3.
+  Qed.
+
+  Next Obligation. (* {{ ⊢ G, A' }} *)
+    clear_defs.
+    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
+  Qed.
+
+  Next Obligation. (* nbe_ty_order G A' *)
+    clear_defs.
+    assert {{ G ⊢ A' : Type@i }} as [? []]%soundness_ty by mauto 4 using alg_type_infer_sound.
+    mauto 3 using nbe_ty_order_sound.
+  Qed.
+
+  Next Obligation. (* {{ G ⊢a λ A' M' ⟹ Π A'' B' }} /\ (exists j, {{ G ⊢a Π A'' B' ⟹ Type@j }}) *)
+    clear_defs.
+    assert {{ G ⊢ A' : Type@i }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ A' ≈ A'' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert {{ ⊢ G, A' }} by mauto 2.
+    assert {{ G ⊢ A'' : Type@i }} by (gen_presups; mauto 2).
+    assert {{ ⊢ G, ~(A'' : exp) }} by mauto 2.
+    assert {{ G, A' ⊢ B' : Type@H1 }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A'' : exp) ⊢ B' : Type@H1 }} by mauto 4.
+    assert (user_exp A'') by trivial using user_exp_nf.
+    assert (exists j, {{ G ⊢a A'' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 3).
+    assert (user_exp B') by trivial using user_exp_nf.
+    assert (exists k, {{ G, ~(A'' : exp) ⊢a B' ⟹ Type@k }} /\ k <= H1) as [? []] by (gen_presups; mauto 3).
+    firstorder mauto 3.
+  Qed.
+
+  Next Obligation. (* exists i : nat, {{ G ⊢ n : Type@i }} *)
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    progressive_inversion.
+    eexists; mauto 4 using alg_type_infer_sound.
+  Qed.
+
+  Next Obligation. (* nbe_ty_order G {{{ B[Id,,N'] }}} *)
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    progressive_inversion.
+    assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A : exp) ⊢ B : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ N' : A }} by mauto 3 using alg_type_check_sound.
+    assert {{ G ⊢ B[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%soundness_ty by mauto 3.
+    mauto 3 using nbe_ty_order_sound.
+  Qed.
+
+  Next Obligation. (* {{ G ⊢a M' N' ⟹ B' }} /\ (exists i, {{ G ⊢a B' ⟹ Type@i }}) *)
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    progressive_inversion.
+    split; [mauto 3 |].
+    assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A : exp) ⊢ B : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ B[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert (user_exp B') by trivial using user_exp_nf.
+    assert (exists k, {{ G ⊢a B' ⟹ Type@k }} /\ k <= j) as [? []] by (gen_presups; mauto 3).
+    firstorder.
+  Qed.
+
+  Next Obligation. (* False *)
+    clear_defs.
+    functional_alg_type_infer_rewrite_clear.
+    progressive_inversion.
+    intuition.
+  Qed.
+
+  Next Obligation. (* {{ ⊢ G, B }} *)
+    clear_defs.
+    assert {{ G ⊢ B : Type@i }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
+  Qed.
+
+  Next Obligation. (* {{ G ⊢a Π B C ⟹ Type@(max i j) }} /\ (exists k, {{ G ⊢a Type@(max i j) ⟹ Type@k }}) *)
+    clear_defs.
+    mautosolve 4.
+  Qed.
+
+  Extraction Inline type_check_functional type_infer_functional.
+End type_check.
+
+Section type_check_closed.
+  #[local]
+  Ltac impl_obl_tac := unfold not; intros; mauto 3 using user_exp_to_type_infer_order, type_check_order, type_infer_order.
+
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
+  Equations type_check_closed A (HA : user_exp A) M (HM : user_exp M) : { {{ ⋅ ⊢ M : A }} } + { ~ {{ ⋅ ⊢ M : A }} } :=
+  | A, HA, M, HM =>
+      let*o->b (exist _ UA _) := type_infer {{{ ⋅ }}} _ A _ while _ in
+      let*o->b (exist _ i _) :=  get_level_of_type_nf UA while _ in
+      let*b _ := type_check {{{ ⋅ }}} A _ M _ while _ in
+      pureb _
+  .
+  Next Obligation. (* False *)
+    assert {{ ⊢ ⋅ }} by mauto 2.
+    assert (exists i, {{ ⋅ ⊢ A : Type@i }}) as [i] by (gen_presups; eauto 2).
+    assert (exists j, {{ ⋅ ⊢a A ⟹ Type@j }} /\ j <= i) as [j []] by mauto 3.
+    firstorder.
+  Qed.
+  Next Obligation. (* False *)
+    assert (exists i, {{ ⋅ ⊢ A : Type@i }}) as [i] by (gen_presups; eauto 2).
+    assert (exists j, {{ ⋅ ⊢a A ⟹ Type@j }} /\ j <= i) as [j []] by mauto 3.
+    functional_alg_type_infer_rewrite_clear.
+    intuition.
+  Qed.
+  Next Obligation. (* exists i, {{ ⋅ ⊢ A : Type@i }} *)
+    assert {{ ⊢ ⋅ }} by mauto 2.
+    assert {{ ⋅ ⊢ A : ~n{{{ Type@i }}} }} by mauto 2 using alg_type_infer_sound.
+    simpl in *.
+    firstorder.
+  Qed.
+  Next Obligation. (* {{ ⋅ ⊢ M : A }} *)
+    assert {{ ⊢ ⋅ }} by mauto 2.
+    assert {{ ⋅ ⊢ A : ~n{{{ Type@i }}} }} by mauto 3 using alg_type_infer_sound.
+    simpl in *.
+    mauto 3 using alg_type_check_sound.
+  Qed.
+End type_check_closed.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index ab43a89d..69522341 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -77,6 +77,7 @@
 ./Extraction/Evaluation.v
 ./Extraction/NbE.v
 ./Extraction/Readback.v
-./Extraction/TypeCheck.v
+./Extraction/PseudoMonadic.v
 ./Extraction/Subtyping.v
+./Extraction/TypeCheck.v
 ./LibTactics.v