diff --git a/theories/admissible.v b/theories/admissible.v
index 830ceec..3e48d49 100644
--- a/theories/admissible.v
+++ b/theories/admissible.v
@@ -16,6 +16,70 @@ Proof.
   hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
 Qed.
 
+
+Lemma App_Inv Γ (b a : PTm) U :
+  Γ ⊢ PApp b a ∈ U ->
+  exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
+Proof.
+  move E : (PApp b a) => u hu.
+  move : b a E. elim : Γ u U / hu => //=.
+  - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
+    exists A,B.
+    repeat split => //=.
+    have [i] : exists i, Γ ⊢ PBind PPi A B ∈  PUniv i by sfirstorder use:regularity.
+    hauto lq:on use:bind_inst, E_Refl.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+
+Lemma Abs_Inv Γ (a : PTm) U :
+  Γ ⊢ PAbs a ∈ U ->
+  exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
+Proof.
+  move E : (PAbs a) => u hu.
+  move : a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B i hP _ ha _ a0 [*]. subst.
+    exists A, B. repeat split => //=.
+    hauto lq:on use:E_Refl, Su_Eq.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+
+
+Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
+  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+Proof.
+  move => a b Γ A ha.
+  move /App_Inv : ha.
+  move => [A0][B0][ha][hb]hS.
+  move /Abs_Inv : ha => [A1][B1][ha]hS0.
+  have hb' := hb.
+  move /E_Refl in hb.
+  have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
+  move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
+  move => h.
+  apply : E_Conv; eauto.
+  apply : E_AppAbs; eauto.
+  eauto using T_Conv.
+Qed.
+
+Lemma T_Eta Γ A a B :
+  A :: Γ ⊢ a ∈ B ->
+  A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B.
+Proof.
+  move => ha.
+  have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff.
+  have hΓ : ⊢ Γ by hauto lq:on inv:Wff.
+  eapply T_App' with (B  := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift.
+  econstructor; eauto. sauto l:on use:renaming.
+  apply T_Var => //.
+  by constructor.
+Qed.
+
 Lemma E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
   (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
@@ -46,3 +110,155 @@ Proof.
   have [i] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto l:on use:regularity.
   move : E_Proj2 h; by repeat move/[apply].
 Qed.
+
+Lemma E_FunExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PPi A B ->
+  Γ ⊢ b ∈ PBind PPi A B ->
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B.
+Proof.
+  hauto l:on use:regularity, E_FunExt.
+Qed.
+
+Lemma E_PairExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B. hauto l:on use:regularity, E_PairExt. Qed.
+
+Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 :
+  renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 ->
+  renaming_ok Γ Ξ (funcomp ξ0 ξ1).
+  rewrite /renaming_ok => h0 h1 i A.
+  move => {}/h1 {}/h0.
+  by asimpl.
+Qed.
+
+Lemma E_AppEta Γ (b : PTm) A B :
+  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
+Proof.
+  move => h.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
+  have [j [hA hB]] : exists i, Γ ⊢ A ∈ PUniv i /\ A :: Γ ⊢ B ∈ PUniv i by hauto lq:on use:Bind_Inv.
+  have {i} {}hPi : Γ ⊢ PBind PPi A B ∈ PUniv j by sfirstorder use:T_Bind, wff_mutual.
+  have hΓ : ⊢ A :: Γ by hauto lq:on use:Bind_Inv, Wff_Cons'.
+  have hΓ' :  ⊢ ren_PTm shift A :: A :: Γ by sauto lq:on use:renaming, renaming_shift inv:Wff.
+  apply E_FunExt; eauto.
+  apply T_Abs.
+  eapply T_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  change (PBind _ _ _) with (ren_PTm shift (PBind PPi A B)).
+
+  eapply renaming; eauto.
+  apply renaming_shift.
+  constructor => //.
+  by constructor.
+
+  apply : E_Transitive. simpl.
+  apply E_AppAbs' with (i := j)(A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B); eauto.
+  by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  constructor => //.
+  by constructor.
+  asimpl.
+  eapply T_App' with (A := ren_PTm shift (ren_PTm shift A)) (B := ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B)); cycle 2.
+  constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift.
+  by constructor. asimpl. substify. by asimpl.
+  have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))=  (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl.
+  eapply renaming; eauto. by eauto using renaming_shift, renaming_comp.
+  asimpl. renamify.
+  eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  sauto lq:on use:renaming, renaming_shift, E_Refl.
+  constructor. constructor=>//. constructor.
+Qed.
+
+Lemma Proj1_Inv Γ (a : PTm ) U :
+  Γ ⊢ PProj PL a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
+Proof.
+  move E : (PProj PL a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    eapply regularity in ha.
+    move : ha => [i].
+    move /Bind_Inv => [j][h _].
+    by move /E_Refl /Su_Eq in h.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Proj2_Inv Γ (a : PTm) U :
+  Γ ⊢ PProj PR a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
+Proof.
+  move E : (PProj PR a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    have ha' := ha.
+    eapply regularity in ha.
+    move : ha => [i ha].
+    move /T_Proj1 in ha'.
+    apply : bind_inst; eauto.
+    apply : E_Refl ha'.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Pair_Inv Γ (a b : PTm ) U :
+  Γ ⊢ PPair a b ∈ U ->
+  exists A B, Γ ⊢ a ∈ A /\
+         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
+         Γ ⊢ PBind PSig A B ≲ U.
+Proof.
+  move E : (PPair a b) => u hu.
+  move : a b E. elim : Γ u U / hu => //=.
+  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
+    exists A,B. repeat split => //=.
+    move /E_Refl /Su_Eq : hS. apply.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => a b Γ A.
+  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move /Su_Sig_Proj1 in hS.
+  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair1; eauto.
+Qed.
+
+Lemma E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
+Proof.
+  move => a b Γ A. move /Proj2_Inv.
+  move => [A0][B0][ha]h.
+  have hr := ha.
+  move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
+  have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using  E_ProjPair1 with wt.
+  move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
+  apply : E_Conv; eauto.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair2; eauto.
+Qed.
+
+
+Lemma E_PairEta Γ a A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PPair (PProj PL a) (PProj PR a) ≡ a ∈ PBind PSig A B.
+Proof.
+  move => h.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto use:regularity.
+  apply E_PairExt => //.
+  eapply T_Pair; eauto with wt.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto with wt.
+  apply E_ProjPair2.
+  apply : T_Proj2; eauto with wt.
+Qed.
diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index ab8fe97..4e4e6fd 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -5,7 +5,6 @@ Require Import ssreflect ssrbool.
 Require Import Psatz.
 From stdpp Require Import relations (rtc(..), nsteps(..)).
 Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Cdcl.Itauto.
 
 Module HRed.
   Lemma ToRRed (a b : PTm) : HRed.R a b -> RRed.R a b.
@@ -98,7 +97,7 @@ Proof.
   - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
     exfalso.
     suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf.
-    eapply ne_nf_embed => //=. itauto.
+    eapply ne_nf_embed => //=. sfirstorder b:on.
   - move => p0 p1 hC  h  ?. exfalso.
     have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
     hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
@@ -199,7 +198,7 @@ Proof.
   - move => u v hC /andP [h0 h1] /synsub_to_usub ?.
     exfalso.
     suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf.
-    eapply ne_nf_embed => //=. itauto.
+    eapply ne_nf_embed => //=. sfirstorder b:on.
   - move => p0 p1 hC  h  ?. exfalso.
     have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
     hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
@@ -252,22 +251,6 @@ Proof.
     apply : ctx_eq_subst_one; eauto.
 Qed.
 
-Lemma T_Univ_Raise Γ (a : PTm) i j :
-  Γ ⊢ a ∈ PUniv i ->
-  i <= j ->
-  Γ ⊢ a ∈ PUniv j.
-Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
-
-Lemma Bind_Univ_Inv Γ p (A : PTm) B i :
-  Γ ⊢ PBind p A B ∈ PUniv i ->
-  Γ ⊢ A ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i.
-Proof.
-  move /Bind_Inv.
-  move => [i0][hA][hB]h.
-  move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
-  sfirstorder use:T_Univ_Raise.
-Qed.
-
 Lemma Abs_Pi_Inv Γ (a : PTm) A B :
   Γ ⊢ PAbs a ∈ PBind PPi A B ->
   (cons A Γ) ⊢ a ∈ B.
@@ -288,6 +271,48 @@ Proof.
   by asimpl; rewrite subst_scons_id.
 Qed.
 
+Lemma T_Abs_Neu_Inv Γ (a u : PTm) U :
+  Γ ⊢ PAbs a ∈ U ->
+  Γ ⊢ u ∈ U ->
+  exists Δ V, Δ ⊢ a ∈ V /\ Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero)  ∈ V.
+Proof.
+  move => /[dup] ha' + hu.
+  move /Abs_Inv => [A0][B0][ha]hSu.
+  move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE.
+  have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
+  have ha'' : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
+  have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i
+    by hauto l:on use:regularity.
+  have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j
+      by qauto l:on use:Bind_Inv.
+  have hΓ : ⊢ cons A2 Γ by eauto using Wff_Cons'.
+  set Δ := cons _ _ in hΓ.
+  have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2.
+  apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto.
+  reflexivity.
+  rewrite -/ren_PTm.
+  apply T_Var; eauto using here.
+  rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id.
+  exists Δ, B2. split => //.
+  by move /Abs_Pi_Inv in ha''.
+Qed.
+
+Lemma T_Univ_Raise Γ (a : PTm) i j :
+  Γ ⊢ a ∈ PUniv i ->
+  i <= j ->
+  Γ ⊢ a ∈ PUniv j.
+Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
+
+Lemma Bind_Univ_Inv Γ p (A : PTm) B i :
+  Γ ⊢ PBind p A B ∈ PUniv i ->
+  Γ ⊢ A ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i.
+Proof.
+  move /Bind_Inv.
+  move => [i0][hA][hB]h.
+  move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
+  sfirstorder use:T_Univ_Raise.
+Qed.
+
 Lemma Pair_Sig_Inv Γ (a b : PTm) A B :
   Γ ⊢ PPair a b ∈ PBind PSig A B ->
   Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
@@ -422,6 +447,18 @@ Proof.
   hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
 Qed.
 
+Lemma CE_HRedR (a b b' : PTm) :
+  HRed.R b b' ->
+  a ⇔ b' ->
+  a ⇔ b.
+Proof.
+  hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
+Qed.
+
+Lemma CE_Nf a b :
+  a ↔ b -> a ⇔ b.
+Proof. hauto l:on ctrs:rtc. Qed.
+
 Scheme
   coqeq_neu_ind := Induction for CoqEq_Neu Sort Prop
   with coqeq_ind := Induction for CoqEq Sort Prop
@@ -549,7 +586,8 @@ Proof.
     have [h2 h3] : Γ ⊢ A2 ≲ A0 /\ Γ ⊢ A2 ≲ A1 by hauto l:on use:Su_Pi_Proj1.
     apply E_Conv with (A := PBind PPi A2 B2); cycle 1.
     eauto using E_Symmetric, Su_Eq.
-    apply : E_Abs; eauto. hauto l:on use:regularity.
+    apply : E_Abs; eauto.
+
     apply iha.
     move /Su_Pi_Proj2_Var in hp0.
     apply : T_Conv; eauto.
@@ -570,13 +608,12 @@ Proof.
     have /regularity_sub0 [i' hPi0] := hPi.
     have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi A2 B2.
     apply : E_AppEta; eauto.
-    hauto l:on use:regularity.
     apply T_Conv with (A := A);eauto.
     eauto using Su_Eq.
     move => ?.
     suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi A2 B2
       by eauto using E_Transitive.
-    apply : E_Abs; eauto. hauto l:on use:regularity.
+    apply : E_Abs; eauto.
     apply iha.
     move /Su_Pi_Proj2_Var in hPi'.
     apply : T_Conv; eauto.
@@ -628,7 +665,7 @@ Proof.
     have hA02 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Sig_Proj1.
     have hu'  : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
     move => [:ih0'].
-    apply : E_Transitive; last (apply E_Symmetric; apply : E_PairEta).
+    apply : E_Transitive; last (apply : E_PairEta).
     apply : E_Pair; eauto. hauto l:on use:regularity.
     abstract : ih0'.
     apply ih0. apply : T_Conv; eauto.
@@ -641,7 +678,6 @@ Proof.
     move /E_Symmetric in ih0'.
     move /regularity_sub0 in hA'.
     hauto l:on use:bind_inst.
-    hauto l:on use:regularity.
     eassumption.
   (* Same as before *)
   - move {hAppL}.
@@ -673,8 +709,12 @@ Proof.
     hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive.
 Qed.
 
-Definition algo_metric k (a b : PTm) :=
-  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ EJoin.R va vb /\ size_PTm va + size_PTm vb + i + j <= k.
+Definition term_metric k (a b : PTm) :=
+  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
+
+Lemma term_metric_sym k (a b : PTm) :
+  term_metric k a b -> term_metric k b a.
+Proof. hauto lq:on unfold:term_metric solve+:lia. Qed.
 
 Lemma ne_hne (a : PTm) : ne a -> ishne a.
 Proof. elim : a => //=; sfirstorder b:on. Qed.
@@ -698,37 +738,56 @@ Proof.
   - hauto lq:on use:ne_hne.
 Qed.
 
-Lemma algo_metric_case k (a b : PTm) :
-  algo_metric k a b ->
-  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ algo_metric k' a' b /\ k' < k.
+Lemma term_metric_case k (a b : PTm) :
+  term_metric k a b ->
+  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k.
 Proof.
-  move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
+  move=>[i][j][va][vb][h0] [h1][h2][h3]h4.
   case : a h0 => //=; try firstorder.
   - inversion h0 as [|A B C D E F]; subst.
     hauto qb:on use:ne_hne.
     inversion E; subst => /=.
-    + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
+    + hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
     + sfirstorder qb:on use:ne_hne.
   - inversion h0 as [|A B C D E F]; subst.
     hauto qb:on use:ne_hne.
     inversion E; subst => /=.
-    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
+    + hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
   - inversion h0 as [|A B C D E F]; subst.
     hauto qb:on use:ne_hne.
     inversion E; subst => /=.
-    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
+    + hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia.
+    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
     + sfirstorder use:ne_hne.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
+    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
     + sfirstorder use:ne_hne.
     + sfirstorder use:ne_hne.
 Qed.
 
-Lemma algo_metric_sym k (a b : PTm) :
-  algo_metric k a b -> algo_metric k b a.
-Proof. hauto lq:on unfold:algo_metric solve+:lia. Qed.
+Lemma A_Conf' a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  tm_conf a b ->
+  algo_dom_r a b.
+Proof.
+  move => ha hb.
+  move => ?.
+  apply A_NfNf.
+  apply A_Conf; sfirstorder use:hf_no_hred, hne_no_hred.
+Qed.
+
+Lemma hne_nf_ne (a : PTm ) :
+  ishne a -> nf a -> ne a.
+Proof. case : a => //=. Qed.
+
+Lemma lored_nsteps_renaming k (a b : PTm) (ξ : nat -> nat) :
+  nsteps LoRed.R k a b ->
+  nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b).
+Proof.
+  induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming.
+Qed.
 
 Lemma hred_hne (a b : PTm) :
   HRed.R a b ->
@@ -886,6 +945,18 @@ Proof.
   hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv.
 Qed.
 
+Lemma T_ZeroUniv_Imp' Γ i :
+  Γ ⊢ PZero ∈ PUniv i -> False.
+Proof.
+  hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Zero_Inv.
+Qed.
+
+Lemma T_SucUniv_Imp' Γ (a : PTm) i :
+  Γ ⊢ PSuc a ∈ PUniv i -> False.
+Proof.
+  hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Suc_Inv.
+Qed.
+
 Lemma T_PairUniv_Imp' Γ (a b : PTm) i  :
   Γ ⊢ PPair a b ∈ PUniv i -> False.
 Proof.
@@ -1028,34 +1099,6 @@ Proof.
     exists (S i), a1. hauto lq:on ctrs:nsteps solve+:lia.
 Qed.
 
-Lemma algo_metric_proj k p0 p1 (a0 a1 : PTm) :
-  algo_metric k (PProj p0 a0) (PProj p1 a1) ->
-  ishne a0 ->
-  ishne a1 ->
-  p0 = p1 /\ exists j, j < k /\ algo_metric j a0 a1.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1.
-  move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
-  move => [i0][a2][hi][?]ha02. subst.
-  move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
-  move => [i1][a3][hj][?]ha13. subst.
-  simpl in *.
-  move /EJoin.hne_proj_inj : h4 => [h40 h41]. subst.
-  split => //.
-  exists (k - 1). split. simpl in *; lia.
-  rewrite/algo_metric.
-  do 4 eexists. repeat split; eauto. sfirstorder use:ne_nf.
-  sfirstorder use:ne_nf.
-  lia.
-Qed.
-
-
-Lemma hreds_nf_refl a b  :
-  HRed.nf a ->
-  rtc HRed.R a b ->
-  a = b.
-Proof. inversion 2; sfirstorder. Qed.
-
 Lemma lored_nsteps_app_cong k (a0 a1 b : PTm) :
   nsteps LoRed.R k a0 a1 ->
   ishne a0 ->
@@ -1103,656 +1146,542 @@ Lemma lored_nsteps_pair_inv k (a0 b0 C : PTm ) :
     exists i, (S j), a1, b1. sauto lq:on solve+:lia.
 Qed.
 
-Lemma algo_metric_join k (a b : PTm ) :
-  algo_metric k a b ->
-  DJoin.R a b.
-  rewrite /algo_metric.
-  move => [i][j][va][vb][h0][h1][h2][h3][[v [h40 h41]]]h5.
-  have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
-  have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
-  apply REReds.FromEReds in h40,h41.
-  apply LoReds.ToRReds in h0,h1.
-  apply REReds.FromRReds in h0,h1.
-  rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive.
-Qed.
-
-Lemma algo_metric_pair k (a0 b0 a1 b1 : PTm) :
-  SN (PPair a0 b0) ->
-  SN (PPair a1 b1) ->
-  algo_metric k (PPair a0 b0) (PPair a1 b1) ->
-  exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
-  move => sn0 sn1 /[dup] /algo_metric_join hj.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
-  move : lored_nsteps_pair_inv h0;repeat move/[apply].
-  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
-  move : lored_nsteps_pair_inv h1;repeat move/[apply].
-  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+Lemma term_metric_abs : forall k a b,
+    term_metric k (PAbs a) (PAbs b) ->
+    exists k', k' < k /\ term_metric k' a b.
+Proof.
+  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_abs_inv in hva, hvb.
+  move : hva => [a'][hva]?. subst.
+  move : hvb => [b'][hvb]?. subst.
   simpl in *. exists (k - 1).
-  move /andP : h2 => [h20 h21].
-  move /andP : h3 => [h30 h31].
-  suff : EJoin.R a2 a3 /\ EJoin.R b2 b3 by hauto lq:on solve+:lia.
-  hauto l:on use:DJoin.ejoin_pair_inj.
+  hauto lq:on unfold:term_metric solve+:lia.
 Qed.
 
-Lemma hne_nf_ne (a : PTm ) :
-  ishne a -> nf a -> ne a.
-Proof. case : a => //=. Qed.
-
-Lemma lored_nsteps_renaming k (a b : PTm) (ξ : nat -> nat) :
-  nsteps LoRed.R k a b ->
-  nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b).
+Lemma term_metric_pair : forall k a0 b0 a1 b1,
+    term_metric k (PPair a0 b0) (PPair a1 b1) ->
+    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
 Proof.
-  induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming.
+  move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_pair_inv in hva, hvb.
+  decompose record hva => {hva}.
+  decompose record hvb => {hvb}. subst.
+  simpl in *. exists (k - 1).
+  hauto lqb:on solve+:lia.
 Qed.
 
-Lemma algo_metric_neu_abs k (a0 : PTm) u :
-  algo_metric k u (PAbs a0) ->
+Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1,
+    term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) ->
+    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
+Proof.
+  move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_bind_inv in hva, hvb.
+  decompose record hva => {hva}.
+  decompose record hvb => {hvb}. subst.
+  simpl in *. exists (k - 1).
+  hauto lqb:on solve+:lia.
+Qed.
+
+Lemma term_metric_suc : forall k a b,
+    term_metric k (PSuc a) (PSuc b) ->
+    exists k', k' < k /\ term_metric k' a b.
+Proof.
+  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_suc_inv in hva, hvb.
+  move : hva => [a'][hva]?. subst.
+  move : hvb => [b'][hvb]?. subst.
+  simpl in *. exists (k - 1).
+  hauto lq:on unfold:term_metric solve+:lia.
+Qed.
+
+Lemma term_metric_abs_neu k (a0 : PTm) u :
+  term_metric k (PAbs a0) u ->
   ishne u ->
-  exists j, j < k /\ algo_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)) a0.
+  exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)).
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu.
-  have neva : ne va by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
-  move /lored_nsteps_abs_inv : h1 => [a1][h01]?. subst.
-  exists (k - 1). simpl in *. split. lia.
-  have {}h0 : nsteps LoRed.R i (ren_PTm shift u) (ren_PTm shift va)
-    by eauto using lored_nsteps_renaming.
-  have {}h0 : nsteps LoRed.R i (PApp (ren_PTm shift u) (VarPTm var_zero)) (PApp (ren_PTm shift va) (VarPTm var_zero)).
-  apply lored_nsteps_app_cong => //=.
-  scongruence use:ishne_ren.
-  do 4 eexists. repeat split; eauto.
-  hauto b:on use:ne_nf_ren.
-  have h : EJoin.R (PAbs (PApp (ren_PTm shift va) (VarPTm var_zero))) (PAbs a1) by hauto q:on ctrs:rtc,ERed.R.
-  apply DJoin.ejoin_abs_inj; eauto.
-  hauto b:on drew:off use:ne_nf_ren.
-  simpl in *.  rewrite size_PTm_ren. lia.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
+  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
+  move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst.
+  exists (k - 1).
+  simpl in *. split. lia.
+  exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)).
+  repeat split => //=.
+  apply lored_nsteps_app_cong.
+  by apply lored_nsteps_renaming.
+  by rewrite ishne_ren.
+  rewrite Bool.andb_true_r.
+  sfirstorder use:ne_nf_ren.
+  rewrite size_PTm_ren. lia.
 Qed.
 
-Lemma algo_metric_neu_pair k (a0 b0 : PTm) u :
-  algo_metric k u (PPair a0 b0) ->
+Lemma term_metric_pair_neu k (a0 b0 : PTm) u :
+  term_metric k (PPair a0 b0) u ->
   ishne u ->
-  exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0.
+  exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0.
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu.
-  move /lored_nsteps_pair_inv : h1.
-  move => [i0][j0][a1][b1][hi][hj][?][ha01]hb01. subst.
-  simpl in *.
-  have ? : ishne va by
-    hauto lq:on use:loreds_hne_preservation, @relations.rtc_nsteps.
-  have ? : ne va by sfirstorder use:hne_nf_ne.
-  exists (k - 1). split. lia.
-  move :lored_nsteps_proj_cong (neu) h0; repeat move/[apply].
-  move => h. have hL := h PL. have {h} hR := h PR.
-  suff [? ?] : EJoin.R (PProj PL va) a1  /\ EJoin.R (PProj PR va) b1.
-  rewrite /algo_metric.
-  split; do 4 eexists; repeat split;eauto; sfirstorder b:on solve+:lia.
-  eapply DJoin.ejoin_pair_inj; hauto qb:on ctrs:rtc, ERed.R.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
+  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
+  move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst.
+  exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia.
 Qed.
 
-Lemma algo_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 :
-  algo_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
+Lemma term_metric_app k (a0 b0 a1 b1 : PTm) :
+  term_metric k (PApp a0 b0) (PApp a1 b1) ->
   ishne a0 ->
   ishne a1 ->
-  exists j, j < k /\ algo_metric j P0 P1 /\ algo_metric j a0 a1 /\
-         algo_metric j b0 b1 /\ algo_metric j c0 c1.
+  exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1.
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1.
-  move /lored_nsteps_ind_inv /(_ hne0) : h0.
-  move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
-  move /lored_nsteps_ind_inv /(_ hne1) : h1.
-  move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
-  move /EJoin.ind_inj : h4.
-  move => [?][?][?]?.
-  exists (k -1). simpl in *.
-  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
-Qed.
-
-Lemma algo_metric_app k (a0 b0 a1 b1 : PTm) :
-  algo_metric k (PApp a0 b0) (PApp a1 b1) ->
-  ishne a0 ->
-  ishne a1 ->
-  exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4.
   move => hne0 hne1.
   move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply].
   move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
   move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply].
   move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
-  simpl in *. exists (k - 1).
-  move /andP : h2 => [h20 h21].
-  move /andP : h3 => [h30 h31].
-  move /EJoin.hne_app_inj : h4 => [h40 h41].
-  split. lia.
-  split.
-  + rewrite /algo_metric.
-    exists i0,j0,a2,a3.
-    repeat split => //=.
-    sfirstorder b:on use:ne_nf.
-    sfirstorder b:on use:ne_nf.
-    lia.
-  + rewrite /algo_metric.
-    exists i1,j1,b2,b3.
-    repeat split => //=; sfirstorder b:on use:ne_nf.
+  simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia.
 Qed.
 
-Lemma algo_metric_suc k (a0 a1 : PTm) :
-  algo_metric k (PSuc a0) (PSuc a1) ->
-  exists j, j < k /\ algo_metric j a0 a1.
+Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) :
+  term_metric k (PProj p0 a0) (PProj p1 a1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ term_metric j a0 a1.
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
-  exists (k - 1).
-  move /lored_nsteps_suc_inv : h0.
-  move => [a0'][ha0]?. subst.
-  move /lored_nsteps_suc_inv : h1.
-  move => [b0'][hb0]?. subst. simpl in *.
-  split; first by lia.
-  rewrite /algo_metric.
-  hauto lq:on rew:off use:EJoin.suc_inj solve+:lia.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
+  move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
+  move => [i0][a2][hi][?]ha02. subst.
+  move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
+  move => [i1][a3][hj][?]ha13. subst.
+  exists (k- 1).  hauto q:on use:ne_nf solve+:lia.
 Qed.
 
-Lemma algo_metric_bind k p0 (A0 : PTm ) B0 p1 A1 B1  :
-  algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
-  p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1.
+Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 :
+  term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\
+         term_metric j b0 b1 /\ term_metric j c0 c1.
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
-  move : lored_nsteps_bind_inv h0 => /[apply].
-  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
-  move : lored_nsteps_bind_inv h1 => /[apply].
-  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
-  move /EJoin.bind_inj : h4 => [?][hEa]hEb. subst.
-  split => //.
-  exists (k - 1). split. simpl in *; lia.
-  simpl in *.
-  split.
-  - exists i0,j0,a2,a3.
-    repeat split => //=; sfirstorder b:on solve+:lia.
-  - exists i1,j1,b2,b3. sfirstorder b:on solve+:lia.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
+  move /lored_nsteps_ind_inv /(_ hne0) : h0.
+  move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
+  move /lored_nsteps_ind_inv /(_ hne1) : h1.
+  move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
+  exists (k -1). simpl in *.
+  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
 Qed.
 
-
-Lemma coqeq_complete' k (a b : PTm ) :
-  algo_metric k a b ->
-  (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\
-  (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
+Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
 Proof.
-  move : k a b.
+  move => [:hneL].
   elim /Wf_nat.lt_wf_ind.
-  move => n ih.
-  move => a b /[dup] h /algo_metric_case. move : a b h => [:hstepL].
-  move => a b h.
-  (* Cases where a and b can take steps *)
-  case; cycle 1.
-  move : ih a b h.
-  abstract : hstepL. qauto l:on use:HRed.preservation, CE_HRedL, hred_hne.
-  move  /algo_metric_sym /algo_metric_case : (h).
-  case; cycle 1.
-  move /algo_metric_sym : h.
-  move : hstepL ih => /[apply]/[apply].
-  repeat move /[apply].
-  move => hstepL.
-  hauto lq:on use:coqeq_symmetric_mutual, algo_metric_sym.
-  (* Cases where a and b can't take wh steps *)
-  move {hstepL}.
-  move : a b h. move => [:hnfneu].
-  move => a b h.
-  case => fb; case => fa.
-  - split; last by sfirstorder use:hf_not_hne.
-    move {hnfneu}.
-    case : a h fb fa => //=.
-    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_AbsNat_Imp.
-      move => a0 a1 ha0 _ _ Γ A wt0 wt1.
-      move : T_Abs_Inv wt0 wt1; repeat move/[apply]. move  => [Δ [V [wt1 wt0]]].
-      apply : CE_HRed; eauto using rtc_refl.
-      apply CE_AbsAbs.
-      suff [l [h0 h1]] : exists l, l < n /\ algo_metric l a1 a0 by eapply ih; eauto.
-      have ? : n > 0 by sauto solve+:lia.
-      exists (n - 1). split; first by lia.
-      move : (ha0). rewrite /algo_metric.
-      move => [i][j][va][vb][hr0][hr1][nfva][nfvb][[v [hr0' hr1']]] har.
-      apply lored_nsteps_abs_inv in hr0, hr1.
-      move : hr0 => [va' [hr00 hr01]].
-      move : hr1 => [vb' [hr10 hr11]]. move {ih}.
-      exists i,j,va',vb'. subst.
-      suff [v0 [hv00 hv01]] : exists v0, rtc ERed.R va' v0 /\ rtc ERed.R vb' v0.
-      repeat split =>//=. sfirstorder.
-      simpl in *; by lia.
-      move /algo_metric_join /DJoin.symmetric : ha0.
-      have : SN a0 /\ SN a1 by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
-      move => /[dup] [[ha00 ha10]] [].
-      move : DJoin.abs_inj; repeat move/[apply].
-      move : DJoin.standardization ha00 ha10; repeat move/[apply].
-      (* this is awful *)
-      move => [vb][va][h' [h'' [h''' [h'''' h'''''']]]].
-      have /LoReds.ToRReds {}hr00 : rtc LoRed.R a1 va'
-        by hauto lq:on use:@relations.rtc_nsteps.
-      have /LoReds.ToRReds {}hr10 : rtc LoRed.R a0 vb'
-        by hauto lq:on use:@relations.rtc_nsteps.
-      simpl in *.
-      have [*] : va' = va /\ vb' = vb by eauto using red_uniquenf. subst.
-      sfirstorder.
-    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp, T_PairNat_Imp, T_PairSuc_Imp, T_PairZero_Imp.
-      move => a1 b1 a0 b0 h _ _ Γ A hu0 hu1.
-      have [sn0 sn1] : SN (PPair a0 b0) /\ SN (PPair a1 b1)
-        by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
-      apply : CE_HRed; eauto using rtc_refl.
-      move /Pair_Inv : hu0 => [A0][B0][ha0][hb0]hSu0.
-      move /Pair_Inv : hu1 => [A1][B1][ha1][hb1]hSu1.
-      move /Sub_Bind_InvR :  (hSu0).
-      move => [i][A2][B2]hE.
-      have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2
-        by eauto using Su_Transitive, Su_Eq.
-      have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2
-        by eauto using Su_Transitive, Su_Eq.
-      have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1.
-      have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1.
-      have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
-      have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
-      move /algo_metric_pair : h sn0 sn1; repeat move/[apply].
-      move => [j][hj][ih0 ih1].
-      have haE : a0 ⇔ a1 by hauto l:on.
-      apply CE_PairPair => //.
-      have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2
-        by hauto l:on use:coqeq_sound_mutual.
-      have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2.
-      apply : T_Conv; eauto.
-      move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2.
-      eapply ih; cycle -1; eauto.
-      apply : T_Conv; eauto.
-      apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2).
-      move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2.
-      move : hE haE. clear.
-      move => h.
-      eapply regularity in h.
-      move : h => [_ [hB _]].
-      eauto using bind_inst.
-    + case : b => //=.
-      * hauto lq:on use:T_AbsBind_Imp.
-      * hauto lq:on rew:off use:T_PairBind_Imp.
-      * move => p1 A1 B1 p0 A0 B0.
-        move /algo_metric_bind.
-        move => [?][j [ih0 [ih1 ih2]]]_ _. subst.
-        move => Γ A hU0 hU1.
-        move /Bind_Inv : hU0 => [i0 [hA0 [hB0 hS0]]].
-        move /Bind_Inv : hU1 => [i1 [hA1 [hB1 hS1]]].
-        have ? : Γ ⊢ PUniv i0 ≲ PUniv (max i0 i1)
-          by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
-        have ? : Γ ⊢ PUniv i1 ≲ PUniv (max i0 i1)
-          by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
-        have {}hA0 : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv.
-        have {}hA1 : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv.
-        have {}hB0 : (cons A0 Γ) ⊢ B0 ∈ PUniv (max i0 i1)
-          by hauto lq:on use:T_Univ_Raise solve+:lia.
-        have {}hB1 : (cons A1 Γ) ⊢ B1 ∈ PUniv (max i0 i1)
-          by hauto lq:on use:T_Univ_Raise solve+:lia.
+  move => n ih a b h.
+  case /term_metric_case : (h); cycle 1.
+  move => [k'][a'][h0][h1]h2.
+  by apply : A_HRedL; eauto.
+  case /term_metric_sym /term_metric_case : (h); cycle 1.
+  move => [k'][b'][hb][/term_metric_sym h0]h1.
+  move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
+  by apply : A_HRedR; eauto.
+  move => /[swap].
+  case => hfa; case => hfb.
+  - move : hfa hfb h.
+    case : a; case : b => //=; eauto 5 using A_Conf' with adom.
+    + hauto lq:on use:term_metric_abs db:adom.
+    + hauto lq:on use:term_metric_pair db:adom.
+    + hauto lq:on use:term_metric_bind db:adom.
+    + hauto lq:on use:term_metric_suc db:adom.
+  - abstract : hneL n ih a b h hfa hfb.
+    case : a hfa h => //=.
+    + hauto lq:on use:term_metric_abs_neu db:adom.
+    + scrush use:term_metric_pair_neu db:adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+  - hauto q:on use:algo_dom_sym, term_metric_sym.
+  - move {hneL}.
+    case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom.
+    + move => a0 b0 a1 b1 nfa0 nfa1.
+      move /term_metric_app /(_ nfa0  nfa1) => [j][hj][ha]hb.
+      apply A_NfNf.
+      (* apply A_NfNf. apply A_NeuNeu. apply A_AppCong => //; eauto. *)
+      have nfa0' : HRed.nf a0 by sfirstorder use:hne_no_hred.
+      have nfb0' : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      have ha0 : algo_dom a0 a1 by eauto using algo_dom_r_algo_dom.
+      constructor => //. eauto.
+    + move => p0 A0 p1 A1 neA0 neA1.
+      have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred.
+      have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred.
+      hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom.
+    + move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1.
+      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
+      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
+Qed.
 
-        have ihA : A0 ⇔ A1 by hauto l:on.
-        have hAE : Γ ⊢ A0 ≡ A1 ∈ PUniv (Nat.max i0 i1)
-          by hauto l:on use:coqeq_sound_mutual.
-        apply : CE_HRed; eauto using rtc_refl.
-        constructor => //.
+Lemma ce_neu_neu_helper a b :
+  ishne a -> ishne b ->
+  (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
+Proof. sauto lq:on. Qed.
 
-        eapply ih; eauto.
-        apply : ctx_eq_subst_one; eauto.
-        eauto using Su_Eq.
-      * move => > /algo_metric_join.
-        hauto lq:on use:DJoin.bind_univ_noconf.
-      * move => > /algo_metric_join.
-        hauto lq:on use:Sub.nat_bind_noconf, Sub.FromJoin.
-      * move => > /algo_metric_join.
-        clear. hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
-      * move => > /algo_metric_join. clear.
-        hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv.
-    + case : b => //=.
-      * hauto lq:on use:T_AbsUniv_Imp.
-      * hauto lq:on use:T_PairUniv_Imp.
-      * qauto l:on use:algo_metric_join, DJoin.bind_univ_noconf, DJoin.symmetric.
-      * move => i j /algo_metric_join /DJoin.univ_inj ? _ _ Γ A hi hj.
-        subst.
-        hauto l:on.
-      * move => > /algo_metric_join.
-        hauto lq:on use:Sub.nat_univ_noconf, Sub.FromJoin.
-      * move => > /algo_metric_join.
-        clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
-      * move => > /algo_metric_join.
-        clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.suc_inv.
-    + case : b => //=.
-      * qauto l:on use:T_AbsNat_Imp.
-      * qauto l:on use:T_PairNat_Imp.
-      * move => > /algo_metric_join /Sub.FromJoin. hauto l:on use:Sub.bind_nat_noconf.
-      * move => > /algo_metric_join /Sub.FromJoin. hauto lq:on use:Sub.univ_nat_noconf.
-      * hauto l:on.
-      * move /algo_metric_join.
-        hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
-      * move => > /algo_metric_join.
-        hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
-    (* Zero *)
-    + case : b => //=.
-      * hauto lq:on rew:off use:T_AbsZero_Imp.
-      * hauto lq: on use: T_PairZero_Imp.
-      * move =>> /algo_metric_join.
-        hauto lq:on rew:off use:REReds.zero_inv, REReds.bind_inv.
-      * move =>> /algo_metric_join.
-        hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
-      * move =>> /algo_metric_join.
-        hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
-      * hauto l:on.
-      * move =>> /algo_metric_join.
-        hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
-    (* Suc *)
-    + case : b => //=.
-      * hauto lq:on rew:off use:T_AbsSuc_Imp.
-      * hauto lq:on use:T_PairSuc_Imp.
-      * move => > /algo_metric_join.
-        hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
-      * move => > /algo_metric_join.
-        hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
-      * move => > /algo_metric_join.
-        hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
-      * move => > /algo_metric_join.
-        hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
-      * move => a0 a1 h _ _.
-        move /algo_metric_suc : h => [j [h4 h5]].
-        move => Γ A /Suc_Inv [h0 h1] /Suc_Inv [h2 h3].
-        move : ih h4 h5;do!move/[apply].
-        move => [ih _].
-        move : ih h0 h2;do!move/[apply].
-        move => h. apply : CE_HRed; eauto using rtc_refl.
-        by constructor.
-  - move : a b h fb fa. abstract : hnfneu.
-    move => + b.
-    case : b => //=.
-    (* NeuAbs *)
-    + move => a u halg _ nea. split => // Γ A hu /[dup] ha.
-      move /Abs_Inv => [A0][B0][_]hSu.
-      move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE.
-      have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
-      have {}ha : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
-      have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i
-        by hauto l:on use:regularity.
-      have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j
-          by qauto l:on use:Bind_Inv.
-      have hΓ : ⊢ cons A2 Γ by eauto using Wff_Cons'.
-      set Δ := cons _ _ in hΓ.
-      have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2.
-      apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto.
-      reflexivity.
-      rewrite -/ren_PTm.
-      apply T_Var; eauto using here.
-      rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id.
-      move /Abs_Pi_Inv in ha.
-      move /algo_metric_neu_abs /(_ nea) : halg.
-      move => [j0][hj0]halg.
-      apply : CE_HRed; eauto using rtc_refl.
-      eapply CE_NeuAbs => //=.
-      eapply ih; eauto.
-    (* NeuPair *)
-    + move => a0 b0 u halg _ neu.
-      split => // Γ A hu /[dup] wt.
-      move /Pair_Inv => [A0][B0][ha0][hb0]hU.
-      move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE.
-      have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on.
-      have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
-      move /Pair_Sig_Inv : wt => [{}ha0 {}hb0].
-      have /T_Proj1 huL := hu.
-      have /T_Proj2 {hu} huR := hu.
-      move /algo_metric_neu_pair /(_ neu) : halg => [j [hj [hL hR]]].
-      have heL : PProj PL u ⇔ a0 by hauto l:on.
-      eapply CE_HRed; eauto using rtc_refl.
-      apply CE_NeuPair; eauto.
-      eapply ih; eauto.
-      apply : T_Conv; eauto.
-      have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i
-        by hauto l:on use:regularity.
-      have /E_Symmetric : Γ ⊢ PProj PL u  ≡ a0 ∈ A2 by
-        hauto l:on use:coqeq_sound_mutual.
-      hauto l:on use:bind_inst.
-    (* NeuBind: Impossible *)
-    + move => b p p0 a /algo_metric_join h _ h0. exfalso.
-      move : h h0. clear.
-      move /Sub.FromJoin.
-      hauto l:on use:Sub.hne_bind_noconf.
-    (* NeuUniv: Impossible *)
-    + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
-    + hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join.
-    (* Zero *)
-    + case => //=.
-      * move => i /algo_metric_join. clear.
-        hauto lq:on rew:off use:REReds.var_inv, REReds.zero_inv.
-      * move => >/algo_metric_join. clear.
-        hauto lq:on rew:off use:REReds.hne_app_inv, REReds.zero_inv.
-      * move => >/algo_metric_join. clear.
-        hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.zero_inv.
-      * move => >/algo_metric_join. clear.
-        move => h _ h2. exfalso.
-        hauto q:on use:REReds.hne_ind_inv, REReds.zero_inv.
-    (* Suc *)
-    + move => a0.
-      case => //=; move => >/algo_metric_join; clear.
-      * hauto lq:on rew:off use:REReds.var_inv, REReds.suc_inv.
-      * hauto lq:on rew:off use:REReds.hne_app_inv, REReds.suc_inv.
-      * hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.suc_inv.
-      * hauto q:on use:REReds.hne_ind_inv, REReds.suc_inv.
-  - move {ih}.
-    move /algo_metric_sym in h.
-    qauto l:on use:coqeq_symmetric_mutual.
-  - move {hnfneu}.
-    (* Clear out some trivial cases *)
-    suff : (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ (exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)).
-    move => h0.
-    split. move => *. apply : CE_HRed; eauto using rtc_refl. apply CE_NeuNeu. by firstorder.
-    by firstorder.
+Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
+  ishne u0 -> ishne u1 ->
+  DJoin.R (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) ->
+  DJoin.R P0 P1 /\ DJoin.R u0 u1 /\ DJoin.R b0 b1 /\ DJoin.R c0 c1.
+Proof. hauto q:on use:REReds.hne_ind_inv. Qed.
 
-    case : a h fb fa => //=.
-    + case : b => //=; move => > /algo_metric_join.
-      * move /DJoin.var_inj => i _ _. subst.
-        move => Γ A B /Var_Inv [? [B0 [h0 h1]]].
-        move /Var_Inv => [_ [C0 [h2 h3]]].
-        have ? : B0 = C0 by eauto using lookup_deter. subst.
-        sfirstorder use:T_Var.
-      * clear => ? ? _. exfalso.
-        hauto l:on use:REReds.var_inv, REReds.hne_app_inv.
-      * clear => ? ? _. exfalso.
-        hauto l:on use:REReds.var_inv, REReds.hne_proj_inv.
-      * clear => ? ? _. exfalso.
-        hauto q:on use:REReds.var_inv, REReds.hne_ind_inv.
-    + case : b => //=;
-                   lazymatch goal with
-                   | [|- context[algo_metric _ (PApp _ _) (PApp _ _)]] => idtac
-                   | _ => move => > /algo_metric_join
-                   end.
-      * clear => *. exfalso.
-        hauto lq:on rew:off use:REReds.hne_app_inv, REReds.var_inv.
-      (* real case *)
-      * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
-        move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
-        move /App_Inv : wtB => [A1][B1][hb1][ha1]hS1.
-        move : algo_metric_app (hne0) (hne1) halg. repeat move/[apply].
-        move => [j [hj [hal0 hal1]]].
-        have /ih := hal0.
-        move /(_ hj).
-        move => [_ ihb].
-        move : ihb (hne0) (hne1) hb0 hb1. repeat move/[apply].
-        move => [hb01][C][hT0][hT1][hT2]hT3.
-        move /Sub_Bind_InvL : (hT0).
-        move => [i][A2][B2]hE.
-        have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
-          eauto using Su_Eq, Su_Transitive.
-        have hSu10 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by
-          eauto using Su_Eq, Su_Transitive.
-        have hSuA0 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
-        have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
-        have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
-        have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
-        move : ih (hj) hal1. repeat move/[apply].
-        move => [ih _].
-        move : ih (ha0') (ha1'); repeat move/[apply].
-        move => iha.
-        split. qblast.
-        exists (subst_PTm (scons a0 VarPTm) B2).
-        split.
-        apply : Su_Transitive; eauto.
-        move /E_Refl in ha0.
-        hauto l:on use:Su_Pi_Proj2.
-        have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual.
-        split.
-        apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2).
-        move /regularity_sub0 : hSu10 => [i0].
-        hauto l:on use:bind_inst.
-        hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl.
-        split.
-        by apply : T_App; eauto using T_Conv_E.
-        apply : T_Conv; eauto.
-        apply T_App with (A := A2) (B := B2); eauto.
-        apply : T_Conv_E; eauto.
-        move /E_Symmetric in h01.
-        move /regularity_sub0 : hSu20 => [i0].
-        sfirstorder use:bind_inst.
-      * clear => ? ? ?. exfalso.
-        hauto q:on use:REReds.hne_app_inv, REReds.hne_proj_inv.
-      * clear => ? ? ?. exfalso.
-        hauto q:on use:REReds.hne_app_inv, REReds.hne_ind_inv.
-    + case : b => //=.
-      * move => i p h /algo_metric_join. clear => ? _ ?. exfalso.
-        hauto l:on use:REReds.hne_proj_inv, REReds.var_inv.
-      * move => > /algo_metric_join. clear => ? ? ?. exfalso.
-        hauto l:on use:REReds.hne_proj_inv, REReds.hne_app_inv.
-      (* real case *)
-      * move => p1 a1 p0 a0 /algo_metric_proj ha hne1 hne0.
-        move : ha (hne0) (hne1); repeat move/[apply].
-        move => [? [j []]]. subst.
-        move : ih; repeat move/[apply].
-        move => [_ ih].
-        case : p1.
-        ** move => Γ A B ha0 ha1.
-           move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
-           move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
-           move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
-           move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
-           split. sauto lq:on.
-           move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
-           have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
-             by eauto using Su_Transitive, Su_Eq.
-           have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
-             by eauto using Su_Transitive, Su_Eq.
-           exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive.
-           repeat split => //=.
-           hauto l:on use:Su_Sig_Proj1, Su_Transitive.
-           apply T_Proj1 with (B := B2); eauto using T_Conv_E.
-           apply T_Proj1 with (B := B2); eauto using T_Conv_E.
-        ** move => Γ A B  ha0  ha1.
-           move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
-           move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
-           move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
-           move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
-           split. sauto lq:on.
-           move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
-           have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
-             by eauto using Su_Transitive, Su_Eq.
-           have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
-             by eauto using Su_Transitive, Su_Eq.
-           have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1.
-           have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1.
-           have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
-           have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
-           have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2
-             by sauto lq:on use:coqeq_sound_mutual.
-           exists (subst_PTm (scons (PProj PL a0) VarPTm) B2).
-           repeat split.
-           *** apply : Su_Transitive; eauto.
-               have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2
-                 by qauto use:regularity, E_Refl.
-               sfirstorder use:Su_Sig_Proj2.
-           *** apply : Su_Transitive; eauto.
-               sfirstorder use:Su_Sig_Proj2.
-           *** eauto using T_Proj2.
-           *** apply : T_Conv.
-               apply : T_Proj2; eauto.
-               move /E_Symmetric in haE.
-               move /regularity_sub0 in hSu21.
-               sfirstorder use:bind_inst.
-      * move => > /algo_metric_join; clear => ? ? ?. exfalso.
-        hauto q:on use:REReds.hne_proj_inv, REReds.hne_ind_inv.
-    (* ind ind case *)
-    + move => P a0 b0 c0.
-      case : b => //=;
-                   lazymatch goal with
-                   | [|- context[algo_metric _ (PInd _ _ _ _) (PInd _ _ _ _)]] => idtac
-                   | _ => move => > /algo_metric_join; clear => *; exfalso
-                   end.
-      * hauto q:on use:REReds.hne_ind_inv, REReds.var_inv.
-      * hauto q:on use:REReds.hne_ind_inv, REReds.hne_app_inv.
-      * hauto q:on use:REReds.hne_ind_inv, REReds.hne_proj_inv.
-      * move => P1 a1 b1 c1 /[dup] halg /algo_metric_ind + h0 h1.
-        move /(_ h1 h0).
-        move => [j][hj][hP][ha][hb]hc Γ A B hL hR.
-        move /Ind_Inv : hL => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
-        move /Ind_Inv : hR => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
-        have {}iha : a0 ∼ a1 by qauto l:on.
-        have []  : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
-        move : T_Univ_Raise wtP0; do!move/[apply]. move => wtP0.
-        move : T_Univ_Raise wtP1; do!move/[apply]. move => wtP1.
-        have {}ihP : P ⇔ P1 by qauto l:on.
-        set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
-        have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
-        have hPE : Δ ⊢ P ≡ P1 ∈ PUniv (max iP0 iP1)
-          by hauto l:on use:coqeq_sound_mutual.
-        have haE : Γ ⊢ a0 ≡ a1 ∈ PNat
-          by hauto l:on use:coqeq_sound_mutual.
-        have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
-        have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
-        eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
-        have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P
-          by eauto using T_Conv_E.
-        have {}ihb : b0 ⇔ b1 by hauto l:on.
-        have hPSig : Γ ⊢ PBind PSig PNat P ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
-        set T := ren_PTm shift _ in wtc0.
-        have : (cons P Δ) ⊢ c1 ∈ T.
-        apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
-        apply : Su_Eq; eauto.
-        subst T. apply : weakening_su; eauto.
-        eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto.
-        hauto l:on use:wff_mutual.
-        apply morphing_ext. set x := funcomp _ _.
-        have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
-        apply : morphing_ren; eauto using renaming_shift. by apply morphing_id.
-        apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
-        have {}ihc : c0 ⇔ c1 by qauto l:on.
-        move => [:ih].
-        split. abstract : ih. move : h0 h1 ihP iha ihb ihc. clear. sauto lq:on.
-        have hEInd : Γ ⊢ PInd P a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P by hfcrush use:coqeq_sound_mutual.
-        exists (subst_PTm (scons a0 VarPTm) P).
-        repeat split => //=; eauto with wt.
-        apply : Su_Transitive.
-        apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
-        apply : Su_Eq. apply E_Refl. by apply T_Nat'.
-        apply : Su_Eq. apply hPE. by eauto.
-        move : hEInd. clear. hauto l:on use:regularity.
+Lemma coqeq_complete' :
+  (forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\
+    (forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
+  move => [:hConfNeuNf hhPairNeu hhAbsNeu].
+  apply algo_dom_mutual.
+  - move => a b h ih hj. split => //.
+    move => Γ A. move : T_Abs_Inv; repeat move/[apply].
+    move => [Δ][V][h0]h1.
+    have [? ?] : SN a /\ SN b by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply CE_Nf. constructor. apply : ih; eauto using DJoin.abs_inj.
+  - abstract : hhAbsNeu.
+    move => a u hu ha iha hj => //.
+    split => //= Γ A.
+    move => + h. have ? : SN u  by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    move : T_Abs_Neu_Inv h; repeat move/[apply].
+    move => [Δ][V][ha']hu'.
+    apply CE_Nf. constructor => //. apply : iha; eauto.
+    apply DJoin.abs_inj.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply : DJoin.transitive; eauto.
+    apply DJoin.symmetric. apply DJoin.FromEJoin. eexists. split. apply relations.rtc_once.
+    apply ERed.AppEta. apply rtc_refl.
+  - hauto q:on use:coqeq_symmetric_mutual, DJoin.symmetric, algo_dom_sym.
+  - move {hhAbsNeu hhPairNeu hConfNeuNf}.
+    move => a0 a1 b0 b1 doma iha domb ihb /DJoin.pair_inj hj.
+    split => //.
+    move => Γ A wt0 wt1.
+    have [] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by hauto lq:on use:logrel.SemWt_SN, fundamental_theorem.
+    move : hj; repeat move/[apply].
+    move => [hja hjb].
+    move /Pair_Inv : wt0 => [A0][B0][ha0][hb0]hSu0.
+    move /Pair_Inv : wt1 => [A1][B1][ha1][hb1]hSu1.
+    move /Sub_Bind_InvR :  (hSu0).
+    move => [i][A2][B2]hE.
+    have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2
+      by eauto using Su_Transitive, Su_Eq.
+    have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2
+      by eauto using Su_Transitive, Su_Eq.
+    have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1.
+    have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1.
+    have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
+    have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
+    move : iha (ha0A2) (ha1A2) hja; repeat move/[apply].
+    move => h.
+    apply CE_Nf.
+    apply CE_PairPair => //.
+    have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2
+      by hauto l:on use:coqeq_sound_mutual.
+    have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2.
+    apply : T_Conv; eauto.
+    move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2.
+    eapply ihb; cycle -1; eauto.
+    apply : T_Conv; eauto.
+    apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2).
+    move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2.
+    move : hE haE. clear.
+    move => h.
+    eapply regularity in h.
+    move : h => [_ [hB _]].
+    eauto using bind_inst.
+  - abstract : hhPairNeu. move {hConfNeuNf}.
+    move => a0 b0 u neu doma iha domb ihb hj.
+    split => // Γ A /[dup] wt /Pair_Inv
+               [A0][B0][ha0][hb0]hU.
+    move => wtu.
+    move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE.
+    have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on.
+    have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+    move /Pair_Sig_Inv : wt => [{}ha0 {}hb0].
+    have /T_Proj1 huL := hu.
+    have /T_Proj2 {hu} huR := hu.
+    have heL : a0 ⇔ PProj PL u . apply : iha; eauto.
+    apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
+    apply : N_Exp; eauto. apply N_ProjPairL.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply DJoin.FromRRed1. apply RRed.ProjPair.
+    eapply CE_HRed; eauto using rtc_refl.
+    apply CE_PairNeu; eauto.
+    eapply ihb; eauto.
+    apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
+    apply : N_Exp; eauto. apply N_ProjPairR.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply DJoin.FromRRed1. apply RRed.ProjPair.
+    apply : T_Conv; eauto.
+    have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i
+      by hauto l:on use:regularity.
+    have /E_Symmetric : Γ ⊢ a0 ≡ PProj PL u ∈ A2 by
+      hauto l:on use:coqeq_sound_mutual.
+    hauto l:on use:bind_inst.
+  - move {hhAbsNeu}.
+    move => a0 a1 u hu  ha iha hb ihb /DJoin.symmetric hj. split => // *.
+    eapply coqeq_symmetric_mutual.
+    eapply algo_dom_sym in ha, hb.
+    eapply hhPairNeu => //=; eauto; hauto lq:on use:DJoin.symmetric, coqeq_symmetric_mutual.
+  - move {hhPairNeu hhAbsNeu}. hauto l:on.
+  - move {hhPairNeu hhAbsNeu}.
+    move => a0 a1 ha iha /DJoin.suc_inj hj. split => //.
+    move => Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
+  - move => i j /DJoin.univ_inj ?. subst.
+    split => //. hauto l:on.
+  - move => {hhPairNeu hhAbsNeu} p0 p1 A0 A1 B0 B1.
+    move => hA ihA hB ihB /DJoin.bind_inj. move => [?][hjA]hjB. subst.
+    split => // Γ A.
+    move => hbd0 hbd1.
+    have {hbd0} : exists i, Γ ⊢ PBind p1 A0 B0 ∈ PUniv i by move /Bind_Inv in hbd0; qauto use:T_Bind.
+    move => [i] => hbd0.
+    have {hbd1} : exists i, Γ ⊢ PBind p1 A1 B1 ∈ PUniv i by move /Bind_Inv in hbd1; qauto use:T_Bind.
+    move => [j] => hbd1.
+    have /Bind_Univ_Inv {hbd0} [? ?] : Γ ⊢ PBind p1 A0 B0 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
+    have /Bind_Univ_Inv {hbd1} [? ?] : Γ ⊢ PBind p1 A1 B1 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
+    move => [:eqa].
+    apply CE_Nf. constructor; first by abstract : eqa; eauto.
+    eapply ihB; eauto. apply : ctx_eq_subst_one; eauto.
+    apply : Su_Eq; eauto. sfirstorder use:coqeq_sound_mutual.
+  - hauto l:on.
+  - move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B.
+    move /Var_Inv => [h [A0 [h0 h1]]].
+    move /Var_Inv => [h' [A1 [h0' h1']]].
+    split. by constructor.
+    suff : A0 = A1 by hauto lq:on db:wt.
+    eauto using lookup_deter.
+  - move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja].
+    apply ce_neu_neu_helper => //= Γ A B.
+    move /App_Inv => [A0][B0][hb0][ha0]hS0.
+    move /App_Inv => [A1][B1][hb1][ha1]hS1.
+    move /(_ hju) : ihu.
+    move => [_ ihb].
+    move : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply].
+    move => [hb01][C][hT0][hT1][hT2]hT3.
+    move /Sub_Bind_InvL : (hT0).
+    move => [i][A2][B2]hE.
+    have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
+      eauto using Su_Eq, Su_Transitive.
+    have hSu10 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by
+      eauto using Su_Eq, Su_Transitive.
+    have hSuA0 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
+    have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
+    have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
+    have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
+    move : iha hja. repeat move/[apply].
+    move => iha.
+    move : iha (ha0') (ha1'); repeat move/[apply].
+    move => iha.
+    split. sauto lq:on.
+    exists (subst_PTm (scons a0 VarPTm) B2).
+    split.
+    apply : Su_Transitive; eauto.
+    move /E_Refl in ha0.
+    hauto l:on use:Su_Pi_Proj2.
+    have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual.
+    split.
+    apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2).
+    move /regularity_sub0 : hSu10 => [i0].
+    hauto l:on use:bind_inst.
+    hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl.
+    split.
+    by apply : T_App; eauto using T_Conv_E.
+    apply : T_Conv; eauto.
+    apply T_App with (A := A2) (B := B2); eauto.
+    apply : T_Conv_E; eauto.
+    move /E_Symmetric in h01.
+    move /regularity_sub0 : hSu20 => [i0].
+    sfirstorder use:bind_inst.
+  - move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst.
+    move : iha hja; repeat move/[apply].
+    move => [_ iha]. apply ce_neu_neu_helper => // Γ A B.
+    move : iha (hne0) (hne1);repeat move/[apply].
+    move => ih.
+    case : p1.
+    ** move => ha0 ha1.
+       move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
+       move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
+       move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
+       move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
+       have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
+         by eauto using Su_Transitive, Su_Eq.
+       have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
+         by eauto using Su_Transitive, Su_Eq.
+       exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive.
+       repeat split => //=.
+       hauto l:on use:Su_Sig_Proj1, Su_Transitive.
+       apply T_Proj1 with (B := B2); eauto using T_Conv_E.
+       apply T_Proj1 with (B := B2); eauto using T_Conv_E.
+    ** move => ha0  ha1.
+       move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
+       move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
+       move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
+       move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
+       have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
+         by eauto using Su_Transitive, Su_Eq.
+       have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
+         by eauto using Su_Transitive, Su_Eq.
+       have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1.
+       have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1.
+       have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+       have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+       have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2
+         by sauto lq:on use:coqeq_sound_mutual.
+       exists (subst_PTm (scons (PProj PL a0) VarPTm) B2).
+       repeat split.
+       *** apply : Su_Transitive; eauto.
+           have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2
+             by qauto use:regularity, E_Refl.
+           sfirstorder use:Su_Sig_Proj2.
+       *** apply : Su_Transitive; eauto.
+           sfirstorder use:Su_Sig_Proj2.
+       *** eauto using T_Proj2.
+       *** apply : T_Conv.
+           apply : T_Proj2; eauto.
+           move /E_Symmetric in haE.
+           move /regularity_sub0 in hSu21.
+           sfirstorder use:bind_inst.
+  - move {hhPairNeu hhAbsNeu}.
+    move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP  domu ihu domb ihb domc ihc /hne_ind_inj.
+    move => /(_ neu0 neu1)  [hjP][hju][hjb]hjc.
+    apply ce_neu_neu_helper => // Γ A B.
+    move /Ind_Inv => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
+    move /Ind_Inv => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
+    have {}iha : u0 ∼ u1 by qauto l:on.
+    have []  : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
+    move : T_Univ_Raise wtP0; repeat move/[apply]. move => wtP0.
+    move : T_Univ_Raise wtP1; repeat move/[apply]. move => wtP1.
+    have {}ihP : P0 ⇔ P1 by qauto l:on.
+    set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
+    have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
+    have hPE : Δ ⊢ P0 ≡ P1 ∈ PUniv (max iP0 iP1)
+      by hauto l:on use:coqeq_sound_mutual.
+    have haE : Γ ⊢ u0 ≡ u1 ∈ PNat
+      by hauto l:on use:coqeq_sound_mutual.
+    have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
+    have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P0 ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
+    eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
+    have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P0
+      by eauto using T_Conv_E.
+    have {}ihb : b0 ⇔ b1 by hauto l:on.
+    have hPSig : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
+    set T := ren_PTm shift _ in wtc0.
+    have : (cons P0 Δ) ⊢ c1 ∈ T.
+    apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
+    apply : Su_Eq; eauto.
+    subst T. apply : weakening_su; eauto.
+    eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto.
+    hauto l:on use:wff_mutual.
+    apply morphing_ext. set x := funcomp _ _.
+    have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
+    apply : morphing_ren; eauto using renaming_shift. by apply morphing_id.
+    apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
+    have {}ihc : c0 ⇔ c1 by qauto l:on.
+    move => [:ih].
+    split. abstract : ih. move : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on.
+    have hEInd : Γ ⊢ PInd P0 u0 b0 c0 ≡ PInd P1 u1 b1 c1 ∈ subst_PTm (scons u0 VarPTm) P0 by hfcrush use:coqeq_sound_mutual.
+    exists (subst_PTm (scons u0 VarPTm) P0).
+    repeat split => //=; eauto with wt.
+    apply : Su_Transitive.
+    apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
+    apply : Su_Eq. apply E_Refl. by apply T_Nat'.
+    apply : Su_Eq. apply hPE. by eauto.
+    move : hEInd. clear. hauto l:on use:regularity.
+  - move => a b ha hb.
+    move {hhPairNeu hhAbsNeu}.
+    case : hb; case : ha.
+    + move {hConfNeuNf}.
+      move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne.
+      move : h0 h1 h2 h3.
+      case : b; case : a => //= *; try by (exfalso; eauto 2 using T_AbsPair_Imp, T_AbsUniv_Imp, T_AbsBind_Imp, T_AbsNat_Imp, T_AbsZero_Imp, T_AbsSuc_Imp,  T_PairUniv_Imp, T_PairBind_Imp, T_PairNat_Imp, T_PairZero_Imp, T_PairSuc_Imp).
+      sfirstorder use:DJoin.bind_univ_noconf.
+      hauto q:on use:REReds.nat_inv, REReds.bind_inv.
+      hauto q:on use:REReds.zero_inv, REReds.bind_inv.
+      hauto q:on use:REReds.suc_inv, REReds.bind_inv.
+      hauto q:on use:REReds.bind_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.bind_inv, REReds.nat_inv.
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
+      hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
+      hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
+      hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
+      hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
+      hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
+      hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
+      hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
+      hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
+    + abstract : hConfNeuNf a b.
+      move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne.
+      move : h0 h1 h2 h3.
+      case : b; case : a => //=; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv, REReds.bind_inv, REReds.nat_inv, REReds.univ_inv, REReds.zero_inv, REReds.suc_inv.
+    + rewrite tm_conf_sym.
+      move => h0 h1 h2 /DJoin.symmetric hb.
+      move : hConfNeuNf h0 h1 h2 hb; repeat move/[apply].
+      qauto l:on use:coqeq_symmetric_mutual.
+    + move => neua neub hconf hj.
+      move {hConfNeuNf}.
+      exfalso.
+      move : neua neub hconf hj.
+      case : b; case : a => //=*; exfalso; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv.
+  - sfirstorder.
+  - move {hConfNeuNf hhPairNeu hhAbsNeu}.
+    move => a a' b hr ha iha hj Γ A wta wtb.
+    apply : CE_HRedL; eauto.
+    apply : iha; eauto; last by sfirstorder use:HRed.preservation.
+    apply : DJoin.transitive; eauto.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply DJoin.FromRRed1. by apply HRed.ToRRed.
+  - move {hConfNeuNf hhPairNeu hhAbsNeu}.
+    move => a b b' nfa hr h ih j Γ A wta wtb.
+    apply : CE_HRedR; eauto.
+    apply : ih; eauto; last by eauto using HRed.preservation.
+    apply : DJoin.transitive; eauto.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply DJoin.FromRRed0. by apply HRed.ToRRed.
 Qed.
 
 Lemma coqeq_sound : forall Γ (a b : PTm) A,
     Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
 Proof. sfirstorder use:coqeq_sound_mutual. Qed.
 
+Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b.
+Proof.
+  move /LoReds.FromSN => [va [ha0 ha1]].
+  move /LoReds.FromSN => [vb [hb0 hb1]].
+  eapply relations.rtc_nsteps in ha0.
+  eapply relations.rtc_nsteps in hb0.
+  hauto lq:on unfold:term_metric solve+:lia.
+Qed.
+
+Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b.
+Proof.
+  move : sn_term_metric; repeat move/[apply].
+  move => [k]+.
+  eauto using term_metric_algo_dom.
+Qed.
+
 Lemma coqeq_complete Γ (a b A : PTm) :
   Γ ⊢ a ≡ b ∈ A -> a ⇔ b.
 Proof.
   move => h.
-  suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity.
-  eapply fundamental_theorem in h.
-  move /logrel.SemEq_SN_Join : h.
-  move => h.
-  have : exists va vb : PTm,
-         rtc LoRed.R a va /\
-         rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb
-      by hauto l:on use:DJoin.standardization_lo.
-  move => [va][vb][hva][hvb][nva][nvb]hj.
-  move /relations.rtc_nsteps : hva => [i hva].
-  move /relations.rtc_nsteps : hvb => [j hvb].
-  exists (i + j + size_PTm va + size_PTm vb).
-  hauto lq:on solve+:lia.
+  have : algo_dom_r a b /\ DJoin.R a b by
+    hauto lq:on use:fundamental_theorem, logrel.SemEq_SemWt, logrel.SemWt_SN, sn_algo_dom.
+  hauto lq:on use:regularity, coqeq_complete'.
 Qed.
 
-
 Reserved Notation "a ≪ b" (at level 70).
 Reserved Notation "a ⋖ b" (at level 70).
 Inductive CoqLEq : PTm -> PTm -> Prop :=
@@ -1794,27 +1723,6 @@ Scheme coqleq_ind := Induction for CoqLEq Sort Prop
 
 Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind.
 
-Definition salgo_metric k (a b : PTm ) :=
-  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ ESub.R va vb /\ size_PTm va + size_PTm vb + i + j <= k.
-
-Lemma salgo_metric_algo_metric k (a b : PTm) :
-  ishne a \/ ishne b ->
-  salgo_metric k a b ->
-  algo_metric k a b.
-Proof.
-  move => h.
-  move => [i][j][va][vb][hva][hvb][nva][nvb][hS]sz.
-  rewrite/ESub.R in hS.
-  move : hS => [va'][vb'][h0][h1]h2.
-  suff : va' = vb' by sauto lq:on.
-  have {}hva : rtc RERed.R a va by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds.
-  have {}hvb : rtc RERed.R b vb by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds.
-  apply REReds.FromEReds in h0, h1.
-  have : ishne va' \/ ishne vb' by
-    hauto lq:on rew:off use:@relations.rtc_transitive, REReds.hne_preservation.
-  hauto lq:on use:Sub1.hne_refl.
-Qed.
-
 Lemma coqleq_sound_mutual :
     (forall (a b : PTm), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\
     (forall (a b : PTm), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ).
@@ -1846,34 +1754,6 @@ Proof.
     eauto using HReds.preservation.
 Qed.
 
-Lemma salgo_metric_case k (a b : PTm ) :
-  salgo_metric k a b ->
-  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ salgo_metric k' a' b /\ k' < k.
-Proof.
-  move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
-  case : a h0 => //=; try firstorder.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
-    + sfirstorder qb:on use:ne_hne.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + sfirstorder use:ne_hne.
-Qed.
-
 Lemma CLE_HRedL (a a' b : PTm )  :
   HRed.R a a' ->
   a' ≪ b ->
@@ -1890,191 +1770,116 @@ Proof.
   hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
 Qed.
 
-
-Lemma algo_metric_caseR k (a b : PTm) :
-  salgo_metric k a b ->
-  (ishf b \/ ishne b) \/ exists k' b', HRed.R b b' /\ salgo_metric k' a b' /\ k' < k.
+Lemma subvar_inj (i j : nat) :
+    Sub.R (VarPTm i) (VarPTm j) -> i = j.
 Proof.
-  move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
-  case : b h1 => //=; try by firstorder.
-  - inversion 1 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto q:on use:HRed.AppAbs unfold:salgo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:salgo_metric solve+:lia.
-    + sfirstorder qb:on use:ne_hne.
-  - inversion 1 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
-  - inversion 1 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + sfirstorder use:ne_hne.
+  rewrite /Sub.R.
+  move => [c][d][h0][h1]h2.
+  apply REReds.var_inv in h0, h1. subst.
+  inversion h2; by subst.
 Qed.
 
-Lemma salgo_metric_sub k (a b : PTm) :
-  salgo_metric k a b ->
-  Sub.R a b.
+Lemma algo_dom_hf_hne (a b : PTm) :
+  algo_dom a b ->
+  (ishf a \/ ishne a) /\ (ishf b \/ ishne b).
 Proof.
-  rewrite /algo_metric.
-  move => [i][j][va][vb][h0][h1][h2][h3][[va' [vb' [hva [hvb hS]]]]]h5.
-  have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
-  have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
-  apply REReds.FromEReds in hva,hvb.
-  apply LoReds.ToRReds in h0,h1.
-  apply REReds.FromRReds in h0,h1.
-  rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive.
+  inversion 1;subst => //=; by sfirstorder b:on.
 Qed.
 
-Lemma salgo_metric_pi k (A0 : PTm) B0 A1 B1  :
-  salgo_metric k (PBind PPi A0 B0) (PBind PPi A1 B1) ->
-  exists j, j < k /\ salgo_metric j A1 A0 /\ salgo_metric j B0 B1.
+Lemma algo_dom_neu_neu_nonconf a b :
+  algo_dom a b ->
+  neuneu_nonconf a b ->
+  ishne a /\ ishne b.
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
-  move : lored_nsteps_bind_inv h0 => /[apply].
-  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
-  move : lored_nsteps_bind_inv h1 => /[apply].
-  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
-  move /ESub.pi_inj : h4 => [? ?].
-  hauto qb:on solve+:lia.
+  move /algo_dom_hf_hne => h.
+  move => h1.
+  destruct a,b => //=; sfirstorder b:on.
 Qed.
 
-Lemma salgo_metric_sig k (A0 : PTm) B0 A1 B1  :
-  salgo_metric k (PBind PSig A0 B0) (PBind PSig A1 B1) ->
-  exists j, j < k /\ salgo_metric j A0 A1 /\ salgo_metric j B0 B1.
+Lemma coqleq_complete' :
+  (forall a b, salgo_dom a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ⋖ b) /\
+  (forall a b, salgo_dom_r a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b).
 Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
-  move : lored_nsteps_bind_inv h0 => /[apply].
-  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
-  move : lored_nsteps_bind_inv h1 => /[apply].
-  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
-  move /ESub.sig_inj : h4 => [? ?].
-  hauto qb:on solve+:lia.
+  apply salgo_dom_mutual.
+  - move => i j /Sub.univ_inj.
+    hauto lq:on ctrs:CoqLEq.
+  - move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i.
+    move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
+    have {}ihA : A1 ≪ A0 by hauto l:on.
+    constructor => //.
+    have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual.
+    suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i
+      by hauto l:on.
+    eauto using ctx_eq_subst_one.
+  - move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i.
+    move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
+    have {}ihA : A0 ≪ A1 by hauto l:on.
+    constructor => //.
+    have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual.
+    suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i
+      by hauto l:on.
+    eauto using ctx_eq_subst_one.
+  - sfirstorder.
+  - move => a b hconf hdom.
+    have [? ?] : ishne a /\ ishne b by sfirstorder use:algo_dom_neu_neu_nonconf.
+    move => h. apply Sub.ToJoin in h; last by tauto.
+    move => Γ i ha hb.
+    apply CLE_NeuNeu. hauto q:on use:coqeq_complete'.
+  - move => [:neunf] a b.
+    case => ha; case => hb.
+    move : ha hb.
+    + case : a => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
+      * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
+        case => + + []//=.
+        hauto lq:on rew:off use:Sub.bind_inj.
+        hauto lq:on rew:off use:Sub.bind_inj.
+        hauto lq:on use:Sub.bind_univ_noconf.
+        hauto lq:on use:Sub.nat_bind_noconf.
+      * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
+        hauto lq:on use:Sub.univ_bind_noconf.
+        hauto lq:on use:Sub.nat_univ_noconf.
+      * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
+        hauto lq:on use:Sub.bind_nat_noconf.
+        hauto lq:on use:Sub.univ_nat_noconf.
+    + move => h0 h1.
+      apply Sub.ToJoin in h1; last by tauto.
+      move => Γ i wta wtb. exfalso.
+      abstract : neunf a b ha hb h0 h1 Γ i wta wtb.
+      case : a ha h0 h1 wta => //=; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'.
+      sfirstorder use: DJoin.hne_bind_noconf.
+      sfirstorder use: DJoin.hne_univ_noconf.
+      sfirstorder use:DJoin.hne_nat_noconf.
+    + move => h0 h1. apply Sub.ToJoin in h1; last by tauto.
+      hauto drew:off use:DJoin.symmetric, stm_conf_sym.
+    + move => h0 h1 Γ i wta wtb.
+      apply CLE_NeuNeu.
+      apply Sub.ToJoin in h1; last by tauto.
+      eapply coqeq_complete'; eauto.
+      apply algo_dom_r_algo_dom.
+      sfirstorder use:hne_no_hred.
+      sfirstorder use:hne_no_hred.
+      hauto lq:on use:sn_algo_dom, logrel.SemWt_SN, fundamental_theorem.
+  - hauto l:on.
+  - move => a a' b hr ha iha hj Γ A wta wtb.
+    apply : CLE_HRedL; eauto.
+    apply : iha; eauto; last by sfirstorder use:HRed.preservation.
+    apply : Sub.transitive; eauto.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply /Sub.FromJoin /DJoin.FromRRed1. by apply HRed.ToRRed.
+  - move => a b b' nfa hr h ih j Γ A wta wtb.
+    apply : CLE_HRedR; eauto.
+    apply : ih; eauto; last by eauto using HRed.preservation.
+    apply : Sub.transitive; eauto.
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
+    apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed.
 Qed.
-
-Lemma coqleq_complete' k (a b : PTm ) :
-  salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b).
-Proof.
-  move : k a b.
-  elim /Wf_nat.lt_wf_ind.
-  move => n ih.
-  move => a b /[dup] h /salgo_metric_case.
-  (* Cases where a and b can take steps *)
-  case; cycle 1.
-  move : a b h.
-  qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne.
-  case /algo_metric_caseR : (h); cycle 1.
-  qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne.
-  (* Cases where neither a nor b can take steps *)
-  case => fb; case => fa.
-  - case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-    + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-      * move => p0 A0 B0 _ p1 A1 B1 _.
-        move => h.
-        have ? : p1 = p0 by
-          hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj.
-        subst.
-        case : p0 h => //=.
-        ** move /salgo_metric_pi.
-           move => [j [hj [hA hB]]] Γ i.
-           move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
-           have ihA : A0 ≪ A1 by hauto l:on.
-           econstructor; eauto using E_Refl; constructor=> //.
-           have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual.
-           suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i
-             by hauto l:on.
-           eauto using ctx_eq_subst_one.
-        ** move /salgo_metric_sig.
-           move => [j [hj [hA hB]]] Γ i.
-           move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
-           have ihA : A1 ≪ A0 by hauto l:on.
-           econstructor; eauto using E_Refl; constructor=> //.
-           have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual.
-           suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i
-             by hauto l:on.
-           eauto using ctx_eq_subst_one.
-      * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf.
-      * hauto lq:on use:salgo_metric_sub, Sub.nat_bind_noconf.
-      * move => _ > _ /salgo_metric_sub.
-        hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv inv:Sub1.R.
-      * hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
-    + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-      * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf.
-      * move => *. econstructor; eauto using rtc_refl.
-        hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong.
-      * hauto lq:on rew:off use:REReds.univ_inv, REReds.nat_inv, salgo_metric_sub inv:Sub1.R.
-      * hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
-      * hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
-  (* Both cases are impossible *)
-    + case : b fb => //=.
-      * hauto lq:on use:T_AbsNat_Imp.
-      * hauto lq:on use:T_PairNat_Imp.
-      * hauto lq:on rew:off use:REReds.nat_inv, REReds.bind_inv, salgo_metric_sub inv:Sub1.R.
-      * hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
-      * hauto l:on.
-      * hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
-      * hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
-    + move => ? ? Γ i /Zero_Inv.
-      clear.
-      move /synsub_to_usub => [_ [_ ]].
-      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
-    + move => ? _ _ Γ i /Suc_Inv => [[_]].
-      move /synsub_to_usub.
-      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
-  - have {}h : DJoin.R a b by
-       hauto lq:on use:salgo_metric_algo_metric, algo_metric_join.
-    case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-    + hauto lq:on use:DJoin.hne_bind_noconf.
-    + hauto lq:on use:DJoin.hne_univ_noconf.
-    + hauto lq:on use:DJoin.hne_nat_noconf.
-    + move => _ _ Γ i _.
-      move /Zero_Inv.
-      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-    + move => p _ _ Γ i _ /Suc_Inv.
-      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-  - have {}h : DJoin.R b a by
-      hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric.
-    case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-    + hauto lq:on use:DJoin.hne_bind_noconf.
-    + hauto lq:on use:DJoin.hne_univ_noconf.
-    + hauto lq:on use:DJoin.hne_nat_noconf.
-    + move => _ _ Γ i.
-      move /Zero_Inv.
-      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-    + move => p _ _ Γ i /Suc_Inv.
-      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-  - move => Γ i ha hb.
-    econstructor; eauto using rtc_refl.
-    apply CLE_NeuNeu. move {ih}.
-    have {}h : algo_metric n a b by
-      hauto lq:on use:salgo_metric_algo_metric.
-    eapply coqeq_complete'; eauto.
-Qed.
-
 Lemma coqleq_complete Γ (a b : PTm) :
   Γ ⊢ a ≲ b -> a ≪ b.
 Proof.
   move => h.
-  suff : exists k, salgo_metric k a b by hauto lq:on use:coqleq_complete', regularity.
-  eapply fundamental_theorem in h.
-  move /logrel.SemLEq_SN_Sub : h.
-  move => h.
-  have : exists va vb : PTm ,
-         rtc LoRed.R a va /\
-         rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb
-      by hauto l:on use:Sub.standardization_lo.
-  move => [va][vb][hva][hvb][nva][nvb]hj.
-  move /relations.rtc_nsteps : hva => [i hva].
-  move /relations.rtc_nsteps : hvb => [j hvb].
-  exists (i + j + size_PTm va + size_PTm vb).
-  hauto lq:on solve+:lia.
+  have : salgo_dom_r a b /\ Sub.R a b by
+    hauto lq:on use:fundamental_theorem, logrel.SemLEq_SemWt, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom.
+  hauto lq:on use:regularity, coqleq_complete'.
 Qed.
 
 Lemma coqleq_sound : forall Γ (a b : PTm) i j,
diff --git a/theories/common.v b/theories/common.v
index 3ea15d6..35267fc 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -1,4 +1,4 @@
-Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect ssrbool.
 From Equations Require Import Equations.
 Derive NoConfusion for nat PTag BTag PTm.
 Derive EqDec for BTag PTag PTm.
@@ -6,6 +6,7 @@ From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
+From stdpp Require Import relations (rtc(..)).
 
 Inductive lookup : nat -> list PTm -> PTm -> Prop :=
 | here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A)
@@ -119,6 +120,26 @@ Definition isabs (a : PTm) :=
   | _ => false
   end.
 
+Definition tm_nonconf (a b : PTm) : bool :=
+  match a, b with
+  | PAbs _, _ => (~~ ishf b) || isabs b
+  | _, PAbs _ => ~~ ishf a
+  | VarPTm _, VarPTm _ => true
+  | PPair _ _, _ => (~~ ishf b) || ispair b
+  | _, PPair _ _ => ~~ ishf a
+  | PZero, PZero => true
+  | PSuc _, PSuc _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | PNat, PNat => true
+  | PUniv _, PUniv _ => true
+  | PBind _ _ _, PBind _ _ _ => true
+  | _,_=> false
+  end.
+
+Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
+
 Definition ishf_ren (a : PTm)  (ξ : nat -> nat) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
@@ -175,3 +196,406 @@ Module HRed.
 
     Definition nf a := forall b, ~ R a b.
 End HRed.
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
+| A_AbsAbs a b :
+  algo_dom_r a b ->
+  (* --------------------- *)
+  algo_dom (PAbs a) (PAbs b)
+
+| A_AbsNeu a u :
+  ishne u ->
+  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
+  (* --------------------- *)
+  algo_dom (PAbs a) u
+
+| A_NeuAbs a u :
+  ishne u ->
+  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
+  (* --------------------- *)
+  algo_dom u (PAbs a)
+
+| A_PairPair a0 a1 b0 b1 :
+  algo_dom_r a0 a1 ->
+  algo_dom_r b0 b1 ->
+  (* ---------------------------- *)
+  algo_dom (PPair a0 b0) (PPair a1 b1)
+
+| A_PairNeu a0 a1 u :
+  ishne u ->
+  algo_dom_r a0 (PProj PL u) ->
+  algo_dom_r a1 (PProj PR u) ->
+  (* ----------------------- *)
+  algo_dom (PPair a0 a1) u
+
+| A_NeuPair a0 a1 u :
+  ishne u ->
+  algo_dom_r (PProj PL u) a0 ->
+  algo_dom_r (PProj PR u) a1 ->
+  (* ----------------------- *)
+  algo_dom u (PPair a0 a1)
+
+| A_ZeroZero :
+  algo_dom PZero PZero
+
+| A_SucSuc a0 a1 :
+  algo_dom_r a0 a1 ->
+  algo_dom (PSuc a0) (PSuc a1)
+
+| A_UnivCong i j :
+  (* -------------------------- *)
+  algo_dom (PUniv i) (PUniv j)
+
+| A_BindCong p0 p1 A0 A1 B0 B1 :
+  algo_dom_r A0 A1 ->
+  algo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
+
+| A_NatCong :
+  algo_dom PNat PNat
+
+| A_VarCong i j :
+  (* -------------------------- *)
+  algo_dom (VarPTm i) (VarPTm j)
+
+| A_AppCong u0 u1 a0 a1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r a0 a1 ->
+  (* ------------------------- *)
+  algo_dom (PApp u0 a0) (PApp u1 a1)
+
+| A_ProjCong p0 p1 u0 u1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  (* ---------------------  *)
+  algo_dom (PProj p0 u0) (PProj p1 u1)
+
+| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom_r P0 P1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r b0 b1 ->
+  algo_dom_r c0 c1 ->
+  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+
+| A_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  tm_conf a b ->
+  algo_dom a b
+
+with algo_dom_r : PTm  -> PTm -> Prop :=
+| A_NfNf a b :
+  algo_dom a b ->
+  algo_dom_r a b
+
+| A_HRedL a a' b  :
+  HRed.R a a' ->
+  algo_dom_r a' b ->
+  (* ----------------------- *)
+  algo_dom_r a b
+
+| A_HRedR a b b'  :
+  HRed.nf a ->
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  (* ----------------------- *)
+  algo_dom_r a b.
+
+Scheme algo_ind := Induction for algo_dom Sort Prop
+  with algor_ind := Induction for algo_dom_r Sort Prop.
+
+Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
+#[export]Hint Constructors algo_dom algo_dom_r : adom.
+
+Definition stm_nonconf a b :=
+  match a, b with
+  | PUniv _, PUniv _ => true
+  | PBind PPi _ _, PBind PPi _ _ => true
+  | PBind PSig _ _, PBind PSig _ _ => true
+  | PNat, PNat => true
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Definition neuneu_nonconf a b :=
+  match a, b with
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Lemma stm_tm_nonconf a b :
+  stm_nonconf a b -> tm_nonconf a b.
+Proof. apply /implyP.
+       destruct a ,b =>//=; hauto lq:on inv:PTag, BTag.
+Qed.
+
+Definition stm_conf a b := ~~ stm_nonconf a b.
+
+Lemma tm_stm_conf a b :
+  tm_conf a b -> stm_conf a b.
+Proof.
+  rewrite /tm_conf /stm_conf.
+  apply /contra /stm_tm_nonconf.
+Qed.
+
+Inductive salgo_dom : PTm -> PTm -> Prop :=
+| S_UnivCong i j :
+  (* -------------------------- *)
+  salgo_dom (PUniv i) (PUniv j)
+
+| S_PiCong  A0 A1 B0 B1 :
+  salgo_dom_r A1 A0 ->
+  salgo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1)
+
+| S_SigCong  A0 A1 B0 B1 :
+  salgo_dom_r A0 A1 ->
+  salgo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1)
+
+| S_NatCong :
+  salgo_dom PNat PNat
+
+| S_NeuNeu a b :
+  neuneu_nonconf a b ->
+  algo_dom a b ->
+  salgo_dom a b
+
+| S_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  stm_conf a b ->
+  salgo_dom a b
+
+with salgo_dom_r : PTm -> PTm -> Prop :=
+| S_NfNf a b :
+  salgo_dom a b ->
+  salgo_dom_r a b
+
+| S_HRedL a a' b  :
+  HRed.R a a' ->
+  salgo_dom_r a' b ->
+  (* ----------------------- *)
+  salgo_dom_r a b
+
+| S_HRedR a b b'  :
+  HRed.nf a ->
+  HRed.R b b' ->
+  salgo_dom_r a b' ->
+  (* ----------------------- *)
+  salgo_dom_r a b.
+
+#[export]Hint Constructors salgo_dom salgo_dom_r : sdom.
+Scheme salgo_ind := Induction for salgo_dom Sort Prop
+  with salgor_ind := Induction for salgo_dom_r Sort Prop.
+
+Combined Scheme salgo_dom_mutual from salgo_ind, salgor_ind.
+
+Lemma hf_no_hred (a b : PTm) :
+  ishf a ->
+  HRed.R a b ->
+  False.
+Proof. hauto l:on inv:HRed.R. Qed.
+
+Lemma hne_no_hred (a b : PTm) :
+  ishne a ->
+  HRed.R a b ->
+  False.
+Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
+
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [_ : is_true (ishne ?a) |- is_true (stm_conf ?a _) ] =>
+      if Constr.is_var a then destruct $a; ltac1:(done) else ()
+  | [|- is_true (stm_conf _ _)] =>
+      unfold stm_conf; ltac1:(done)
+  end.
+
+Ltac destruct_salgo := ltac2:(destruct_salgo ()).
+
+Lemma algo_dom_r_inv a b :
+  algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma A_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  algo_dom_r a' b ->
+  algo_dom_r a b.
+  induction 1; sfirstorder use:A_HRedL.
+Qed.
+
+Lemma A_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  algo_dom a b' ->
+  algo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a.
+Proof. case : a; case : b => //=. Qed.
+
+Lemma algo_dom_no_hred (a b : PTm) :
+  algo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+
+Lemma A_HRedR' a b b' :
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  algo_dom_r a b.
+Proof.
+  move => hb /algo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:algo_dom_no_hred.
+  hauto lq:on use:A_HRedsL, A_HRedsR.
+Qed.
+
+Lemma algo_dom_sym :
+  (forall a b (h : algo_dom a b), algo_dom b a) /\
+    (forall a b (h : algo_dom_r a b), algo_dom_r b a).
+Proof.
+  apply algo_dom_mutual; try qauto use:tm_conf_sym,A_HRedR' db:adom.
+Qed.
+
+Lemma salgo_dom_r_inv a b :
+  salgo_dom_r a b -> exists a0 b0, salgo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma S_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  salgo_dom_r a' b ->
+  salgo_dom_r a b.
+  induction 1; sfirstorder use:S_HRedL.
+Qed.
+
+Lemma S_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  salgo_dom a b' ->
+  salgo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma stm_conf_sym a b : stm_conf a b = stm_conf b a.
+Proof. case : a; case : b => //=; hauto lq:on inv:PTag, BTag. Qed.
+
+Lemma salgo_dom_no_hred (a b : PTm) :
+  salgo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred, algo_dom_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+Lemma S_HRedR' a b b' :
+  HRed.R b b' ->
+  salgo_dom_r a b' ->
+  salgo_dom_r a b.
+Proof.
+  move => hb /salgo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:salgo_dom_no_hred.
+  hauto lq:on use:S_HRedsL, S_HRedsR.
+Qed.
+
+Ltac solve_conf := intros; split;
+      apply S_Conf; solve [destruct_salgo | sfirstorder ctrs:salgo_dom use:hne_no_hred, hf_no_hred].
+
+Ltac solve_basic := hauto q:on ctrs:salgo_dom, salgo_dom_r, algo_dom use:algo_dom_sym.
+
+Lemma algo_dom_salgo_dom :
+  (forall a b, algo_dom a b -> salgo_dom a b /\ salgo_dom b a) /\
+    (forall a b, algo_dom_r a b -> salgo_dom_r a b /\ salgo_dom_r b a).
+Proof.
+  apply algo_dom_mutual => //=; try first [solve_conf | solve_basic].
+  - case; case; hauto lq:on ctrs:salgo_dom use:algo_dom_sym inv:HRed.R unfold:HRed.nf.
+  - move => a b ha hb hc. split;
+      apply S_Conf; hauto l:on use:tm_conf_sym, tm_stm_conf.
+  - hauto lq:on ctrs:salgo_dom_r use:S_HRedR'.
+Qed.
+
+Fixpoint hred (a : PTm) : option (PTm) :=
+    match a with
+    | VarPTm i => None
+    | PAbs a => None
+    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
+    | PApp a b =>
+        match hred a with
+        | Some a => Some (PApp a b)
+        | None => None
+        end
+    | PPair a b => None
+    | PProj p (PPair a b) => if p is PL then Some a else Some b
+    | PProj p a =>
+        match hred a with
+        | Some a => Some (PProj p a)
+        | None => None
+        end
+    | PUniv i => None
+    | PBind p A B => None
+    | PNat => None
+    | PZero => None
+    | PSuc a => None
+    | PInd P PZero b c => Some b
+    | PInd P (PSuc a) b c =>
+        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+    | PInd P a b c =>
+        match hred a with
+        | Some a => Some (PInd P a b c)
+        | None => None
+        end
+    end.
+
+Lemma hred_complete (a b : PTm) :
+  HRed.R a b -> hred a = Some b.
+Proof.
+  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
+Qed.
+
+Lemma hred_sound (a b : PTm):
+  hred a = Some b -> HRed.R a b.
+Proof.
+  elim : a b; hauto q:on dep:on ctrs:HRed.R.
+Qed.
+
+Lemma hred_deter (a b0 b1 : PTm) :
+  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
+Proof.
+  move /hred_complete => + /hred_complete. congruence.
+Qed.
+
+Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
+  destruct (hred a) eqn:eq.
+  right. exists p. by apply hred_sound in eq.
+  left. move => b /hred_complete. congruence.
+Defined.
+
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. Qed.
+
+Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b.
+Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed.
diff --git a/theories/executable.v b/theories/executable.v
index 44557f9..558aa75 100644
--- a/theories/executable.v
+++ b/theories/executable.v
@@ -11,345 +11,6 @@ Set Default Proof Mode "Classic".
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 
-Definition tm_nonconf (a b : PTm) : bool :=
-  match a, b with
-  | PAbs _, _ => (~~ ishf b) || isabs b
-  | _, PAbs _ => ~~ ishf a
-  | VarPTm _, VarPTm _ => true
-  | PPair _ _, _ => (~~ ishf b) || ispair b
-  | _, PPair _ _ => ~~ ishf a
-  | PZero, PZero => true
-  | PSuc _, PSuc _ => true
-  | PApp _ _, PApp _ _ => (~~ ishf a) && (~~ ishf b)
-  | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b)
-  | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b)
-  | PNat, PNat => true
-  | PUniv _, PUniv _ => true
-  | PBind _ _ _, PBind _ _ _ => true
-  | _,_=> false
-  end.
-
-Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
-
-Inductive eq_view : PTm -> PTm -> Type :=
-| V_AbsAbs a b :
-  eq_view (PAbs a) (PAbs b)
-| V_AbsNeu a b :
-  ~~ ishf b ->
-  eq_view (PAbs a) b
-| V_NeuAbs a b :
-  ~~ ishf a ->
-  eq_view a (PAbs b)
-| V_VarVar i j :
-  eq_view (VarPTm i) (VarPTm j)
-| V_PairPair a0 b0 a1 b1 :
-  eq_view (PPair a0 b0) (PPair a1 b1)
-| V_PairNeu a0 b0 u :
-  ~~ ishf u ->
-  eq_view (PPair a0 b0) u
-| V_NeuPair u a1 b1 :
-  ~~ ishf u ->
-  eq_view u (PPair a1 b1)
-| V_ZeroZero :
-  eq_view PZero PZero
-| V_SucSuc a b :
-  eq_view (PSuc a) (PSuc b)
-| V_AppApp u0 b0 u1 b1 :
-  eq_view (PApp u0 b0) (PApp u1 b1)
-| V_ProjProj p0 u0 p1 u1 :
-  eq_view (PProj p0 u0) (PProj p1 u1)
-| V_IndInd P0 u0 b0 c0  P1 u1 b1 c1 :
-  eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
-| V_NatNat :
-  eq_view PNat PNat
-| V_BindBind p0 A0 B0 p1 A1 B1 :
-  eq_view (PBind p0 A0 B0) (PBind p1 A1 B1)
-| V_UnivUniv i j :
-  eq_view (PUniv i) (PUniv j)
-| V_Others a b :
-  tm_conf a b ->
-  eq_view a b.
-
-Equations tm_to_eq_view (a b : PTm) : eq_view a b :=
-  tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b;
-  tm_to_eq_view (PAbs a) (PApp b0 b1) := V_AbsNeu a (PApp b0 b1) _;
-  tm_to_eq_view (PAbs a) (VarPTm i) := V_AbsNeu a (VarPTm i) _;
-  tm_to_eq_view (PAbs a) (PProj p b) := V_AbsNeu a (PProj p b) _;
-  tm_to_eq_view (PAbs a) (PInd P u b c) := V_AbsNeu a (PInd P u b c) _;
-  tm_to_eq_view (VarPTm i) (PAbs a) := V_NeuAbs (VarPTm i) a _;
-  tm_to_eq_view (PApp b0 b1) (PAbs b) := V_NeuAbs (PApp b0 b1) b _;
-  tm_to_eq_view (PProj p b) (PAbs a) := V_NeuAbs (PProj p b) a _;
-  tm_to_eq_view (PInd P u b c) (PAbs a) := V_NeuAbs (PInd P u b c) a _;
-  tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j;
-  tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1;
-  (* tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; *)
-  tm_to_eq_view (PPair a0 b0) (VarPTm i) := V_PairNeu a0 b0 (VarPTm i) _;
-  tm_to_eq_view (PPair a0 b0) (PApp c0 c1) := V_PairNeu a0 b0 (PApp c0 c1) _;
-  tm_to_eq_view (PPair a0 b0) (PProj p c) := V_PairNeu a0 b0 (PProj p c) _;
-  tm_to_eq_view (PPair a0 b0) (PInd P t0 t1 t2) := V_PairNeu a0 b0 (PInd P t0 t1 t2) _;
-  (* tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; *)
-  tm_to_eq_view (VarPTm i) (PPair a1 b1) := V_NeuPair (VarPTm i) a1 b1 _;
-  tm_to_eq_view (PApp t0 t1) (PPair a1 b1) := V_NeuPair (PApp t0 t1) a1 b1 _;
-  tm_to_eq_view (PProj t0 t1) (PPair a1 b1) := V_NeuPair (PProj t0 t1) a1 b1 _;
-  tm_to_eq_view (PInd t0 t1 t2 t3) (PPair a1 b1) := V_NeuPair (PInd t0 t1 t2 t3) a1 b1 _;
-  tm_to_eq_view PZero PZero := V_ZeroZero;
-  tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b;
-  tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1;
-  tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1;
-  tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1;
-  tm_to_eq_view PNat PNat := V_NatNat;
-  tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j;
-  tm_to_eq_view (PBind p0 A0 B0)  (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1;
-  tm_to_eq_view a b := V_Others a b _.
-
-Inductive algo_dom : PTm -> PTm -> Prop :=
-| A_AbsAbs a b :
-  algo_dom_r a b ->
-  (* --------------------- *)
-  algo_dom (PAbs a) (PAbs b)
-
-| A_AbsNeu a u :
-  ishne u ->
-  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
-  (* --------------------- *)
-  algo_dom (PAbs a) u
-
-| A_NeuAbs a u :
-  ishne u ->
-  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
-  (* --------------------- *)
-  algo_dom u (PAbs a)
-
-| A_PairPair a0 a1 b0 b1 :
-  algo_dom_r a0 a1 ->
-  algo_dom_r b0 b1 ->
-  (* ---------------------------- *)
-  algo_dom (PPair a0 b0) (PPair a1 b1)
-
-| A_PairNeu a0 a1 u :
-  ishne u ->
-  algo_dom_r a0 (PProj PL u) ->
-  algo_dom_r a1 (PProj PR u) ->
-  (* ----------------------- *)
-  algo_dom (PPair a0 a1) u
-
-| A_NeuPair a0 a1 u :
-  ishne u ->
-  algo_dom_r (PProj PL u) a0 ->
-  algo_dom_r (PProj PR u) a1 ->
-  (* ----------------------- *)
-  algo_dom u (PPair a0 a1)
-
-| A_ZeroZero :
-  algo_dom PZero PZero
-
-| A_SucSuc a0 a1 :
-  algo_dom_r a0 a1 ->
-  algo_dom (PSuc a0) (PSuc a1)
-
-| A_UnivCong i j :
-  (* -------------------------- *)
-  algo_dom (PUniv i) (PUniv j)
-
-| A_BindCong p0 p1 A0 A1 B0 B1 :
-  algo_dom_r A0 A1 ->
-  algo_dom_r B0 B1 ->
-  (* ---------------------------- *)
-  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
-
-| A_NatCong :
-  algo_dom PNat PNat
-
-| A_VarCong i j :
-  (* -------------------------- *)
-  algo_dom (VarPTm i) (VarPTm j)
-
-| A_ProjCong p0 p1 u0 u1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  (* ---------------------  *)
-  algo_dom (PProj p0 u0) (PProj p1 u1)
-
-| A_AppCong u0 u1 a0 a1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  algo_dom_r a0 a1 ->
-  (* ------------------------- *)
-  algo_dom (PApp u0 a0) (PApp u1 a1)
-
-| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom_r P0 P1 ->
-  algo_dom u0 u1 ->
-  algo_dom_r b0 b1 ->
-  algo_dom_r c0 c1 ->
-  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
-
-| A_Conf a b :
-  HRed.nf a ->
-  HRed.nf b ->
-  tm_conf a b ->
-  algo_dom a b
-
-with algo_dom_r : PTm  -> PTm -> Prop :=
-| A_NfNf a b :
-  algo_dom a b ->
-  algo_dom_r a b
-
-| A_HRedL a a' b  :
-  HRed.R a a' ->
-  algo_dom_r a' b ->
-  (* ----------------------- *)
-  algo_dom_r a b
-
-| A_HRedR a b b'  :
-  HRed.nf a ->
-  HRed.R b b' ->
-  algo_dom_r a b' ->
-  (* ----------------------- *)
-  algo_dom_r a b.
-
-Scheme algo_ind := Induction for algo_dom Sort Prop
-  with algor_ind := Induction for algo_dom_r Sort Prop.
-
-Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
-
-
-(* Inductive salgo_dom : PTm -> PTm -> Prop := *)
-(* | S_UnivCong i j : *)
-(*   (* -------------------------- *) *)
-(*   salgo_dom (PUniv i) (PUniv j) *)
-
-(* | S_PiCong A0 A1 B0 B1 : *)
-(*   salgo_dom_r A1 A0 -> *)
-(*   salgo_dom_r B0 B1 -> *)
-(*   (* ---------------------------- *) *)
-(*   salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1) *)
-
-(* | S_SigCong A0 A1 B0 B1 : *)
-(*   salgo_dom_r A0 A1 -> *)
-(*   salgo_dom_r B0 B1 -> *)
-(*   (* ---------------------------- *) *)
-(*   salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1) *)
-
-(* | S_NatCong : *)
-(*   salgo_dom PNat PNat *)
-
-(* | S_NeuNeu a b : *)
-(*   ishne a -> *)
-(*   ishne b -> *)
-(*   algo_dom a b -> *)
-(*   (* ------------------- *) *)
-(*   salgo_dom *)
-
-(* | S_Conf a b : *)
-(*   HRed.nf a -> *)
-(*   HRed.nf b -> *)
-(*   tm_conf a b -> *)
-(*   salgo_dom a b *)
-
-(* with salgo_dom_r : PTm  -> PTm -> Prop := *)
-(* | S_NfNf a b : *)
-(*   salgo_dom a b -> *)
-(*   salgo_dom_r a b *)
-
-(* | S_HRedL a a' b  : *)
-(*   HRed.R a a' -> *)
-(*   salgo_dom_r a' b -> *)
-(*   (* ----------------------- *) *)
-(*   salgo_dom_r a b *)
-
-(* | S_HRedR a b b'  : *)
-(*   HRed.nf a -> *)
-(*   HRed.R b b' -> *)
-(*   salgo_dom_r a b' -> *)
-(*   (* ----------------------- *) *)
-(*   salgo_dom_r a b. *)
-
-(* Scheme salgo_ind := Induction for salgo_dom Sort Prop *)
-(*   with algor_ind := Induction for salgo_dom_r Sort Prop. *)
-
-
-Lemma hf_no_hred (a b : PTm) :
-  ishf a ->
-  HRed.R a b ->
-  False.
-Proof. hauto l:on inv:HRed.R. Qed.
-
-Lemma hne_no_hred (a b : PTm) :
-  ishne a ->
-  HRed.R a b ->
-  False.
-Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
-
-Lemma algo_dom_no_hred (a b : PTm) :
-  algo_dom a b ->
-  HRed.nf a /\ HRed.nf b.
-Proof.
-  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
-Qed.
-
-Derive Signature for algo_dom algo_dom_r.
-
-Fixpoint hred (a : PTm) : option (PTm) :=
-    match a with
-    | VarPTm i => None
-    | PAbs a => None
-    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
-    | PApp a b =>
-        match hred a with
-        | Some a => Some (PApp a b)
-        | None => None
-        end
-    | PPair a b => None
-    | PProj p (PPair a b) => if p is PL then Some a else Some b
-    | PProj p a =>
-        match hred a with
-        | Some a => Some (PProj p a)
-        | None => None
-        end
-    | PUniv i => None
-    | PBind p A B => None
-    | PNat => None
-    | PZero => None
-    | PSuc a => None
-    | PInd P PZero b c => Some b
-    | PInd P (PSuc a) b c =>
-        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
-    | PInd P a b c =>
-        match hred a with
-        | Some a => Some (PInd P a b c)
-        | None => None
-        end
-    end.
-
-Lemma hred_complete (a b : PTm) :
-  HRed.R a b -> hred a = Some b.
-Proof.
-  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
-Qed.
-
-Lemma hred_sound (a b : PTm):
-  hred a = Some b -> HRed.R a b.
-Proof.
-  elim : a b; hauto q:on dep:on ctrs:HRed.R.
-Qed.
-
-Lemma hred_deter (a b0 b1 : PTm) :
-  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
-Proof.
-  move /hred_complete => + /hred_complete. congruence.
-Qed.
-
-Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
-  destruct (hred a) eqn:eq.
-  right. exists p. by apply hred_sound in eq.
-  left. move => b /hred_complete. congruence.
-Defined.
-
 Ltac2 destruct_algo () :=
   lazy_match! goal with
   | [h : algo_dom ?a ?b |- _ ] =>
@@ -373,70 +34,79 @@ Ltac solve_check_equal :=
   | _ => idtac
   end].
 
-#[derive(equations=no)]Equations check_equal (a b : PTm) (h : algo_dom a b) :
-  bool by struct h :=
-  check_equal a b h with tm_to_eq_view a b :=
-  check_equal _ _ h (V_VarVar i j) := nat_eqdec i j;
-  check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
-  check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
-  check_equal _ _ h (V_PairPair a0 b0 a1 b1) :=
-    check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_PairNeu a0 b0 u _) :=
-    check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv);
-  check_equal _ _ h (V_NeuPair u a1 b1 _) :=
-    check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv);
-  check_equal _ _ h V_NatNat := true;
-  check_equal _ _ h V_ZeroZero := true;
-  check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_ProjProj p0 a p1 b) :=
-    PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_AppApp a0 b0 a1 b1) :=
-    check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) :=
-    check_equal_r P0 P1 ltac:(check_equal_triv) &&
-      check_equal u0 u1 ltac:(check_equal_triv) &&
-      check_equal_r b0 b1 ltac:(check_equal_triv) &&
-      check_equal_r c0 c1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_UnivUniv i j) := nat_eqdec i j;
-  check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) :=
-    BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv);
-  check_equal _ _ _ _ := false
+Global Set Transparent Obligations.
 
-  (* check_equal a b h := false; *)
-  with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
-  bool by struct h0 :=
-    check_equal_r a b h with (fancy_hred a) :=
-      check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _;
-      check_equal_r a b h (inl h')  with (fancy_hred b) :=
-        | inr b' := check_equal_r a (proj1_sig b') _;
-                 | inl h'' := check_equal a b _.
+Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
+
+Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
+  match a, b with
+  | VarPTm i, VarPTm j => nat_eqdec i j
+  | PAbs a, PAbs b => check_equal_r a b _
+  | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PPair a0 b0, PPair a1 b1 =>
+      check_equal_r a0 a1 _ && check_equal_r b0 b1 _
+  | PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PNat, PNat => true
+  | PZero, PZero => true
+  | PSuc a, PSuc b => check_equal_r a b _
+  | PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _
+  | PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _
+  | PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 =>
+      check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _
+  | PUniv i, PUniv j => nat_eqdec i j
+  | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _
+  | _, _ => false
+  end
+with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool :=
+  match fancy_hred a with
+  | inr a' => check_equal_r (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_equal_r a (proj1_sig b') _
+            | inl hb' => check_equal a b _
+            end
+  end.
 
 Next Obligation.
-  intros.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
   inversion h; subst => //=.
-  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
-  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct h.
-  exfalso. sfirstorder use: algo_dom_no_hred.
-  exfalso. sfirstorder.
-  assert (  b' = b'0)by eauto using hred_deter. subst.
-  apply h.
-Defined.
-
-Next Obligation.
-  simpl. intros.
-  inversion h; subst =>//=.
   exfalso. sfirstorder use:algo_dom_no_hred.
-  move {h}.
-  assert (a' = a'0) by eauto using hred_deter, hred_sound. by subst.
-  exfalso. sfirstorder use:hne_no_hred, hf_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
+  exfalso. sfirstorder.
 Defined.
 
+Next Obligation.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
+  destruct b' as [b' hb']. simpl.
+  inversion h; subst.
+  - exfalso.
+    sfirstorder use:algo_dom_no_hred.
+  - exfalso.
+    sfirstorder.
+  - assert (b' = b'0) by eauto using hred_deter. by subst.
+Defined.
+
+(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
+Next Obligation.
+  move => /= a b hdom ha _ hb _.
+  inversion hdom; subst.
+  - assumption.
+  - exfalso; sfirstorder.
+  - exfalso; sfirstorder.
+Defined.
 
 Lemma check_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h.
 Proof. reflexivity. Qed.
@@ -491,14 +161,14 @@ Proof.
   sfirstorder use:hred_complete, hred_sound.
 Qed.
 
+Ltac simp_check_r := with_strategy opaque [check_equal] simpl in *.
+
 Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom.
 Proof.
   have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred.
   have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
-  simpl.
-  rewrite /check_equal_r_functional.
+  simp_check_r.
   destruct (fancy_hred a).
-  simpl.
   destruct (fancy_hred b).
   reflexivity.
   exfalso. hauto l:on use:hred_complete.
@@ -509,11 +179,9 @@ Lemma check_equal_hredl a b a' ha doma :
   check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
 Proof.
   simpl.
-  rewrite /check_equal_r_functional.
   destruct (fancy_hred a).
   - hauto q:on unfold:HRed.nf.
   - destruct s as [x ?].
-    rewrite /check_equal_r_functional.
     have ? : x = a' by eauto using hred_deter. subst.
     simpl.
     f_equal.
@@ -524,7 +192,7 @@ Lemma check_equal_hredr a b b' hu r a0 :
   check_equal_r a b (A_HRedR a b b' hu r a0) =
     check_equal_r a b' a0.
 Proof.
-  simpl. rewrite /check_equal_r_functional.
+  simpl.
   destruct (fancy_hred a).
   - simpl.
     destruct (fancy_hred b) as [|[b'' hb']].
@@ -547,31 +215,51 @@ Proof. destruct a; destruct b => //=. Qed.
 
 #[export]Hint Rewrite check_equal_abs_abs check_equal_abs_neu check_equal_neu_abs check_equal_pair_pair check_equal_pair_neu check_equal_neu_pair check_equal_bind_bind check_equal_hredl check_equal_hredr check_equal_nfnf check_equal_conf : ce_prop.
 
-Obligation Tactic := try solve [check_equal_triv | sfirstorder].
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [h : salgo_dom ?a ?b |- _ ] =>
+      if is_var a then destruct $a; ltac1:(done)  else
+        (if is_var b then destruct $b; ltac1:(done) else ())
+  end.
 
-Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} :=
+Ltac check_sub_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
+  | _ => idtac
+  end.
+
+Local Obligation Tactic := try solve [check_sub_triv | sfirstorder].
+
+Program Fixpoint check_sub (a b : PTm) (h : salgo_dom a b) {struct h} :=
   match a, b with
   | PBind PPi A0 B0, PBind PPi A1 B1 =>
-      check_sub_r (negb q) A0 A1 _ && check_sub_r q B0 B1 _
+      check_sub_r A1 A0 _ && check_sub_r B0 B1 _
   | PBind PSig A0 B0, PBind PSig A1 B1 =>
-      check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _
+      check_sub_r A0 A1 _ && check_sub_r B0 B1 _
   | PUniv i, PUniv j =>
-      if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i
+      PeanoNat.Nat.leb i j
   | PNat, PNat => true
-  | _ ,_ => ishne a && ishne b && check_equal a b h
+  | PApp _ _ , PApp _ _ => check_equal a b _
+  | VarPTm _, VarPTm _ => check_equal a b _
+  | PInd _ _ _ _, PInd _ _ _ _ => check_equal a b _
+  | PProj _ _, PProj _ _ => check_equal a b _
+  | _, _ => false
   end
-with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} :=
+with check_sub_r (a b : PTm) (h : salgo_dom_r a b) {struct h} :=
   match fancy_hred a with
-  | inr a' => check_sub_r q (proj1_sig a') b _
+  | inr a' => check_sub_r (proj1_sig a') b _
   | inl ha' => match fancy_hred b with
-            | inr b' => check_sub_r q a (proj1_sig b') _
-            | inl hb' => check_sub q a b _
+            | inr b' => check_sub_r a (proj1_sig b') _
+            | inl hb' => check_sub  a b _
             end
   end.
+
 Next Obligation.
   simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
   inversion h; subst => //=.
-  exfalso. sfirstorder use:algo_dom_no_hred.
+  exfalso. sfirstorder use:salgo_dom_no_hred.
   assert (a' = a'0) by eauto using hred_deter. by subst.
   exfalso. sfirstorder.
 Defined.
@@ -581,7 +269,7 @@ Next Obligation.
   destruct b' as [b' hb']. simpl.
   inversion h; subst.
   - exfalso.
-    sfirstorder use:algo_dom_no_hred.
+    sfirstorder use:salgo_dom_no_hred.
   - exfalso.
     sfirstorder.
   - assert (b' = b'0) by eauto using hred_deter. by subst.
@@ -589,34 +277,30 @@ Defined.
 
 (* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
 Next Obligation.
-  move => _ /= a b hdom ha _ hb _.
+  move => /= a b hdom ha _ hb _.
   inversion hdom; subst.
   - assumption.
   - exfalso; sfirstorder.
   - exfalso; sfirstorder.
 Defined.
 
-Lemma check_sub_pi_pi q A0 B0  A1 B1 h0 h1 :
-  check_sub q (PBind PPi A0 B0) (PBind PPi A1 B1) (A_BindCong PPi PPi A0 A1 B0 B1 h0 h1) =
-    check_sub_r (~~ q) A0 A1 h0 && check_sub_r q B0 B1 h1.
+Lemma check_sub_pi_pi A0 B0  A1 B1 h0 h1 :
+  check_sub (PBind PPi A0 B0) (PBind PPi A1 B1) (S_PiCong A0 A1 B0 B1 h0 h1) =
+    check_sub_r A1 A0 h0 && check_sub_r B0 B1 h1.
 Proof. reflexivity. Qed.
 
-Lemma check_sub_sig_sig q A0 B0  A1 B1 h0 h1 :
-  check_sub q (PBind PSig A0 B0) (PBind PSig A1 B1) (A_BindCong PSig PSig A0 A1 B0 B1 h0 h1) =
-    check_sub_r q A0 A1 h0 && check_sub_r q B0 B1 h1.
-  reflexivity. Qed.
+Lemma check_sub_sig_sig A0 B0  A1 B1 h0 h1 :
+  check_sub (PBind PSig A0 B0) (PBind PSig A1 B1) (S_SigCong A0 A1 B0 B1 h0 h1) =
+    check_sub_r A0 A1 h0 && check_sub_r B0 B1 h1.
+Proof. reflexivity. Qed.
 
 Lemma check_sub_univ_univ i j :
-  check_sub true (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb i j.
+  check_sub (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j.
 Proof. reflexivity. Qed.
 
-Lemma check_sub_univ_univ' i j :
-  check_sub false (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb j i.
-  reflexivity. Qed.
-
-Lemma check_sub_nfnf q a b dom : check_sub_r q a b (A_NfNf a b dom) = check_sub q a b dom.
+Lemma check_sub_nfnf a b dom : check_sub_r a b (S_NfNf a b dom) = check_sub a b dom.
 Proof.
-  have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred.
+  have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
   have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
   simpl.
   destruct (fancy_hred b)=>//=.
@@ -627,8 +311,8 @@ Proof.
   hauto l:on use:hred_complete.
 Qed.
 
-Lemma check_sub_hredl q a b a' ha doma :
-  check_sub_r q a b (A_HRedL a a' b ha doma) = check_sub_r q a' b doma.
+Lemma check_sub_hredl a b a' ha doma :
+  check_sub_r a b (S_HRedL a a' b ha doma) = check_sub_r a' b doma.
 Proof.
   simpl.
   destruct (fancy_hred a).
@@ -640,9 +324,9 @@ Proof.
     apply PropExtensionality.proof_irrelevance.
 Qed.
 
-Lemma check_sub_hredr q a b b' hu r a0 :
-  check_sub_r q a b (A_HRedR a b b' hu r a0) =
-    check_sub_r q a b' a0.
+Lemma check_sub_hredr a b b' hu r a0 :
+  check_sub_r a b (S_HRedR a b b' hu r a0) =
+    check_sub_r a b' a0.
 Proof.
   simpl.
   destruct (fancy_hred a).
@@ -657,4 +341,10 @@ Proof.
     sfirstorder use:hne_no_hred, hf_no_hred.
 Qed.
 
-#[export]Hint Rewrite check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ' check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.
+Lemma check_sub_neuneu a b i a0 : check_sub a b (S_NeuNeu a b i a0) = check_equal a b a0.
+Proof. destruct a,b => //=. Qed.
+
+Lemma check_sub_conf a b n n0 i : check_sub a b (S_Conf a b n n0 i) = false.
+Proof. destruct a,b=>//=; ecrush inv:BTag. Qed.
+
+#[export]Hint Rewrite check_sub_neuneu check_sub_conf check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.
diff --git a/theories/executable_correct.v b/theories/executable_correct.v
index 6ccee46..40debce 100644
--- a/theories/executable_correct.v
+++ b/theories/executable_correct.v
@@ -23,6 +23,14 @@ Proof.
   inversion 3; subst => //=.
 Qed.
 
+Lemma coqeq_neuneu' u0 u1 :
+  neuneu_nonconf u0 u1 ->
+  u0 ↔ u1 ->
+  u0 ∼ u1.
+Proof.
+  induction 2 => //=; destruct u => //=.
+Qed.
+
 Lemma check_equal_sound :
   (forall a b (h : algo_dom a b), check_equal a b h -> a ↔ b) /\
   (forall a b (h : algo_dom_r a b), check_equal_r a b h -> a ⇔ b).
@@ -63,15 +71,15 @@ Proof.
   - sfirstorder.
   - move => i j /sumboolP ?.  subst.
     apply : CE_NeuNeu. apply CE_VarCong.
+  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
+    rewrite check_equal_app_app in hE.
+    move /andP : hE => [h0 h1].
+    sauto lq:on use:coqeq_neuneu.
   - move => p0 p1 u0 u1 neu0 neu1 h ih he.
     apply CE_NeuNeu.
     rewrite check_equal_proj_proj in he.
     move /andP : he => [/sumboolP ? h1]. subst.
     sauto lq:on use:coqeq_neuneu.
-  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
-    rewrite check_equal_app_app in hE.
-    move /andP : hE => [h0 h1].
-    sauto lq:on use:coqeq_neuneu.
   - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
     rewrite check_equal_ind_ind.
     move /andP => [/andP [/andP [h0 h1] h2 ] h3].
@@ -117,14 +125,14 @@ Proof.
   - simp check_equal. done.
   - move => i j. move => h. have {h} : ~ nat_eqdec i j by done.
     case : nat_eqdec => //=. ce_solv.
+  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
+    rewrite check_equal_app_app.
+    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
   - move => p0 p1 u0 u1 neu0 neu1 h ih.
     rewrite check_equal_proj_proj.
     move /negP /nandP. case.
     case : PTag_eqdec => //=. sauto lq:on.
     sauto lqb:on.
-  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
-    rewrite check_equal_app_app.
-    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
   - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
     rewrite check_equal_ind_ind.
     move => + h.
@@ -172,39 +180,31 @@ Qed.
 
 Ltac simp_sub := with_strategy opaque [check_equal] simpl in *.
 
-(* Reusing algo_dom results in an inefficient proof, but i'll brute force it so i can get the result more quickly *)
 Lemma check_sub_sound :
-  (forall a b (h : algo_dom a b), forall q, check_sub q a b h -> if q then a ⋖ b else b ⋖ a) /\
-    (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h -> if q then a ≪ b else b ≪ a).
+  (forall a b (h : salgo_dom a b), check_sub a b h -> a ⋖ b) /\
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h -> a ≪ b).
 Proof.
-  apply algo_dom_mutual; try done.
-  - move => a [] //=; hauto qb:on.
-  - move => a0 a1 []//=; hauto qb:on.
+  apply salgo_dom_mutual; try done.
   - simpl. move => i j [];
     sauto lq:on use:Reflect.Nat_leb_le.
-  - move => p0 p1 A0 A1 B0 B1 a iha b ihb q.
-    case : p0; case : p1; try done; simp ce_prop.
-    sauto lqb:on.
-    sauto lqb:on.
-  - hauto l:on.
-  - move => i j q h.
-    have {}h : nat_eqdec i j by sfirstorder.
-    case : nat_eqdec h => //=; sauto lq:on.
-  - simp_sub.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
-  - simp_sub.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
-  - simp_sub.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
-  - move => a b n n0 i q h.
-    exfalso.
-    destruct a, b; try done; simp_sub; hauto lb:on use:check_equal_conf.
-  - move => a b doma ihdom q.
-    simp ce_prop. sauto lq:on.
-  - move => a a' b hr doma ihdom q.
-    simp ce_prop. move : ihdom => /[apply]. move {doma}.
-    sauto lq:on.
-  - move => a b b' n r dom ihdom q.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
+    simp ce_prop.
+    hauto lqb:on ctrs:CoqLEq.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
+    simp ce_prop.
+    hauto lqb:on ctrs:CoqLEq.
+  - qauto ctrs:CoqLEq.
+  - move => a b i a0.
+    simp ce_prop.
+    move => h. apply CLE_NeuNeu.
+    hauto lq:on use:check_equal_sound, coqeq_neuneu', coqeq_symmetric_mutual.
+  - move => a b n n0 i.
+    by simp ce_prop.
+  - move => a b h ih. simp ce_prop. hauto l:on.
+  - move => a a' b hr h ih.
+    simp ce_prop.
+    sauto lq:on rew:off.
+  - move => a b b' n r dom ihdom.
     simp ce_prop.
     move : ihdom => /[apply].
     move {dom}.
@@ -212,91 +212,48 @@ Proof.
 Qed.
 
 Lemma check_sub_complete :
-  (forall a b (h : algo_dom a b), forall q, check_sub q a b h = false -> if q then ~ a ⋖ b else ~ b ⋖ a) /\
-    (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h = false -> if q then ~ a ≪ b else ~ b ≪ a).
+  (forall a b (h : salgo_dom a b), check_sub a b h = false -> ~ a ⋖ b) /\
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h = false -> ~ a ≪ b).
 Proof.
-  apply algo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
-  - move => i j q /=.
-    sauto lq:on rew:off use:PeanoNat.Nat.leb_le.
-  - move => p0 p1 A0 A1 B0 B1 a iha b ihb [].
-    + move => + h. inversion h; subst; simp ce_prop.
-      * move /nandP.
-        case.
-        by move => /negbTE {}/iha.
-        by move => /negbTE {}/ihb.
-      * move /nandP.
-        case.
-        by move => /negbTE {}/iha.
-        by move => /negbTE {}/ihb.
-      * inversion H.
-    + move => + h. inversion h; subst; simp ce_prop.
-      * move /nandP.
-        case.
-        by move => /negbTE {}/iha.
-        by move => /negbTE {}/ihb.
-      * move /nandP.
-        case.
-        by move => /negbTE {}/iha.
-        by move => /negbTE {}/ihb.
-      * inversion H.
-  - simp_sub.
-    sauto lq:on use:check_equal_complete.
-  - simp_sub.
-    move => p0 p1 u0 u1 i i0 a iha q.
+  apply salgo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
+  - move => i j /=.
+    move => + h. inversion h; subst => //=.
+    sfirstorder use:PeanoNat.Nat.leb_le.
+    hauto lq:on inv:CoqEq_Neu.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
     move /nandP.
     case.
-    move /nandP.
-    case => //.
-    by move /negP.
-    by move /negP.
-    move /negP.
-    move => h. eapply check_equal_complete in h.
-    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
-  - move => u0 u1 a0 a1 i i0 a hdom ihdom hdom' ihdom'.
-    simp_sub.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
     move /nandP.
     case.
-    move/nandP.
-    case.
-    by move/negP.
-    by move/negP.
-    move /negP.
-    move => h. eapply check_equal_complete in h.
-    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
-  - move => P0 P1 u0 u1 b0 b1 c0 c1 i i0 dom ihdom dom' ihdom' dom'' ihdom'' dom''' ihdom''' q.
-    move /nandP.
-    case.
-    move /nandP.
-    case => //=.
-    by move/negP.
-    by move/negP.
-    move /negP => h. eapply check_equal_complete in h.
-    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
-  - move => a b h ih q. simp ce_prop => {}/ih.
-    case : q => h0;
-    inversion 1; subst; hauto l:on use:algo_dom_no_hred, hreds_nf_refl.
-  - move => a a' b r dom ihdom q.
-    simp ce_prop => {}/ihdom.
-    case : q => h0.
-    inversion 1; subst.
-    inversion H0; subst. sfirstorder use:coqleq_no_hred.
-    have ? : a' = y by eauto using hred_deter. subst.
-    sauto lq:on.
-    inversion 1; subst.
-    inversion H1; subst. sfirstorder use:coqleq_no_hred.
-    have ? : a' = y by eauto using hred_deter. subst.
-    sauto lq:on.
-  - move => a b b' n r hr ih q.
-    simp ce_prop => {}/ih.
-    case : q.
-    + move => h. inversion 1; subst.
-      inversion H1; subst.
-      sfirstorder use:coqleq_no_hred.
-      have ? : b' = y by eauto using hred_deter. subst.
-      sauto lq:on.
-    + move => h. inversion 1; subst.
-      inversion H0; subst.
-      sfirstorder use:coqleq_no_hred.
-      have ? : b' = y by eauto using hred_deter. subst.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
+  - move => a b i hs. simp ce_prop.
+    move => + h. inversion h; subst => //=.
+    move => /negP h0.
+    eapply check_equal_complete in h0.
+    apply h0. by constructor.
+  - move => a b s ihs. simp ce_prop.
+    move => h0 h1. apply ihs =>//.
+    have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
+    inversion h1; subst.
+    hauto l:on use:hreds_nf_refl.
+  - move => a a' b h dom.
+    simp ce_prop => /[apply].
+    move => + h1. inversion h1; subst.
+    inversion H; subst.
+    + sfirstorder use:coqleq_no_hred unfold:HRed.nf.
+    + have ? : y = a' by eauto using hred_deter. subst.
       sauto lq:on.
+  - move => a b b' u hr dom ihdom.
+    rewrite check_sub_hredr.
+    move => + h. inversion h; subst.
+    have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred.
+    move => {}/ihdom.
+    inversion H0; subst.
+    + have ? : HRed.nf b'0 by hauto l:on use:coqleq_no_hred.
+      sfirstorder unfold:HRed.nf.
+    + sauto lq:on use:hred_deter.
 Qed.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 9d8718b..382f25b 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -10,7 +10,7 @@ From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
 From Hammer Require Import Tactics.
 Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 Require Import Btauto.
-Require Import Cdcl.Itauto.
+
 
 Ltac2 spec_refl () :=
   List.iter
@@ -2575,7 +2575,7 @@ Module LoReds.
     ~~ ishf a.
   Proof.
     move : hf_preservation. repeat move/[apply].
-    case : a; case : b => //=; itauto.
+    case : a; case : b => //=; sfirstorder b:on.
   Qed.
 
   #[local]Ltac solve_s_rec :=
@@ -2633,7 +2633,7 @@ Module LoReds.
     rtc LoRed.R (PSuc a0) (PSuc a1).
   Proof. solve_s. Qed.
 
-  Local Ltac triv := simpl in *; itauto.
+  Local Ltac triv := simpl in *; sfirstorder b:on.
 
   Lemma FromSN_mutual :
     (forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\
@@ -3048,7 +3048,7 @@ Module DJoin.
     have {h0 h1 h2 h3} : isbind c /\ isuniv c by
       hauto l:on use:REReds.bind_preservation,
           REReds.univ_preservation.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma hne_univ_noconf (a b : PTm) :
@@ -3078,7 +3078,7 @@ Module DJoin.
   Proof.
     move => [c [h0 h1]] h2 h3.
     have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation.
-    clear. case : c => //=; itauto.
+    clear. case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :
@@ -3594,7 +3594,7 @@ Module Sub.
       hauto l:on use:REReds.bind_preservation,
             REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
     move : h2 h3. clear.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma univ_bind_noconf (a b : PTm) :
@@ -3605,7 +3605,7 @@ Module Sub.
       hauto l:on use:REReds.bind_preservation,
             REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
     move : h2 h3. clear.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :
diff --git a/theories/logrel.v b/theories/logrel.v
index a479f81..e11659e 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -6,7 +6,7 @@ Require Import ssreflect ssrbool.
 Require Import Logic.PropExtensionality (propositional_extensionality).
 From stdpp Require Import relations (rtc(..), rtc_subrel).
 Import Psatz.
-Require Import Cdcl.Itauto.
+
 
 Definition ProdSpace (PA : PTm -> Prop)
   (PF : PTm -> (PTm -> Prop) -> Prop) b : Prop :=
@@ -355,7 +355,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : SNe H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       move : hA hAB. clear. hauto lq:on db:noconf.
       move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
       tauto.
@@ -365,7 +365,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : SNe H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       move : hAB hA h0. clear. hauto lq:on db:noconf.
       move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
       tauto.
@@ -375,7 +375,7 @@ Proof.
       have {hU} {}h : Sub.R (PBind p A B) H
         by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have{h0} : isbind H.
-      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       have : isbind (PBind p A B) by scongruence.
       move : h. clear. hauto l:on db:noconf.
       case : H h1 h => //=.
@@ -394,7 +394,7 @@ Proof.
       have {hU} {}h : Sub.R H (PBind p A B)
         by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have{h0} : isbind H.
-      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       have : isbind (PBind p A B) by scongruence.
       move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
       case : H h1 h => //=.
@@ -413,7 +413,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : isnat H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on.
       have : @isnat PNat by simpl.
       move : h0 hAB. clear. qauto l:on db:noconf.
       case : H h1 hAB h0 => //=.
@@ -424,7 +424,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : isnat H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on.
       have : @isnat PNat by simpl.
       move : h0 hAB. clear. qauto l:on db:noconf.
       case : H h1 hAB h0 => //=.
@@ -619,10 +619,6 @@ Proof.
   split; apply : InterpUniv_cumulative; eauto.
 Qed.
 
-(* Semantic context wellformedness *)
-Definition SemWff Γ := forall (i : nat) A, lookup i Γ A -> exists j, Γ ⊨ A ∈ PUniv j.
-Notation "⊨ Γ" := (SemWff Γ) (at level 70).
-
 Lemma ρ_ok_id Γ :
   ρ_ok Γ VarPTm.
 Proof.
@@ -763,6 +759,34 @@ Proof.
   move : weakening_Sem h0 h1; repeat move/[apply]. done.
 Qed.
 
+Reserved Notation "⊨ Γ"  (at level 70).
+
+Inductive SemWff : list PTm -> Prop :=
+| SemWff_nil :
+  ⊨ nil
+| SemWff_cons Γ A i :
+  ⊨ Γ ->
+  Γ ⊨ A ∈ PUniv i ->
+  (* -------------- *)
+  ⊨ (cons A Γ)
+where "⊨ Γ" := (SemWff Γ).
+
+(* Semantic context wellformedness *)
+Lemma SemWff_lookup Γ :
+  ⊨ Γ ->
+  forall (i : nat) A, lookup i Γ A -> exists j, Γ ⊨ A ∈ PUniv j.
+Proof.
+  move => h. elim : Γ / h.
+  - by inversion 1.
+  - move => Γ A i hΓ ihΓ hA  j B.
+    elim /lookup_inv => //=_.
+    + move => ? ? ? [*]. subst.
+      eauto using weakening_Sem_Univ.
+    + move => i0 Γ0 A0 B0 hl ? [*]. subst.
+      move : ihΓ hl => /[apply]. move => [j hA0].
+      eauto using weakening_Sem_Univ.
+Qed.
+
 Lemma SemWt_SN Γ (a : PTm) A :
   Γ ⊨ a ∈ A ->
   SN a /\ SN A.
@@ -784,25 +808,6 @@ Lemma SemLEq_SN_Sub Γ (a b : PTm) :
   SN a /\ SN b /\ Sub.R a b.
 Proof. hauto l:on use:SemLEq_SemWt, SemWt_SN. Qed.
 
-(* Structural laws for Semantic context wellformedness *)
-Lemma SemWff_nil : SemWff nil.
-Proof. hfcrush inv:lookup. Qed.
-
-Lemma SemWff_cons Γ (A : PTm) i :
-    ⊨ Γ ->
-    Γ ⊨ A ∈ PUniv i ->
-    (* -------------- *)
-    ⊨ (cons A Γ).
-Proof.
-  move => h h0.
-  move => j A0.  elim/lookup_inv => //=_.
-  - hauto q:on use:weakening_Sem.
-  - move => i0 Γ0 A1 B + ? [*]. subst.
-    move : h => /[apply]. move => [k hk].
-    exists k. change (PUniv k) with (ren_PTm shift (PUniv k)).
-    eauto using weakening_Sem.
-Qed.
-
 (* Semantic typing rules *)
 Lemma ST_Var' Γ (i : nat) A j :
   lookup i Γ A ->
@@ -819,7 +824,7 @@ Lemma ST_Var Γ (i : nat) A :
   ⊨ Γ ->
   lookup i Γ A ->
   Γ ⊨ VarPTm i ∈ A.
-Proof. hauto l:on use:ST_Var' unfold:SemWff. Qed.
+Proof. hauto l:on use:ST_Var', SemWff_lookup. Qed.
 
 Lemma InterpUniv_Bind_nopf p i (A : PTm) B PA :
   ⟦ A ⟧ i ↘ PA ->
@@ -1058,7 +1063,7 @@ Definition Γ_sub' Γ Δ := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ.
 Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ.
 
 Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ.
-  rewrite /Γ_sub'. itauto. Qed.
+  rewrite /Γ_sub'. sfirstorder b:on. Qed.
 
 Lemma Γ_sub'_cons Γ Δ A B i j :
   Sub.R B A ->
@@ -1516,6 +1521,36 @@ Proof.
   rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
 Qed.
 
+Lemma SE_PairExt Γ (a b : PTm) A B i :
+  Γ ⊨ PBind PSig A B ∈ PUniv i ->
+  Γ ⊨ a ∈ PBind PSig A B ->
+  Γ ⊨ b ∈ PBind PSig A B ->
+  Γ ⊨ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊨ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊨ a ≡ b ∈ PBind PSig A B.
+Proof.
+  move => h0 ha hb h1 h2.
+  suff h : Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B /\
+           Γ ⊨ PPair (PProj PL b) (PProj PR b) ≡ b ∈ PBind PSig A B /\
+           Γ ⊨ PPair (PProj PL a) (PProj PR a) ≡ PPair (PProj PL b) (PProj PR b) ∈ PBind PSig A B
+    by decompose [and] h; eauto using SE_Transitive, SE_Symmetric.
+  eauto 20 using SE_PairEta, SE_Symmetric, SE_Pair.
+Qed.
+
+Lemma SE_FunExt Γ (a b : PTm) A B i :
+  Γ ⊨ PBind PPi A B ∈ PUniv i ->
+  Γ ⊨ a ∈ PBind PPi A B ->
+  Γ ⊨ b ∈ PBind PPi A B ->
+  A :: Γ ⊨ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊨ a ≡ b ∈ PBind PPi A B.
+Proof.
+  move => hpi ha hb he.
+  move : SE_Abs (hpi) he. repeat move/[apply]. move => he.
+  have /SE_Symmetric : Γ ⊨ PAbs (PApp (ren_PTm shift a) (VarPTm var_zero)) ≡ a ∈ PBind PPi A B by eauto using SE_AppEta.
+  have : Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B by eauto using SE_AppEta.
+  eauto using SE_Transitive.
+Qed.
+
 Lemma SE_Nat Γ (a b : PTm) :
   Γ ⊨ a ≡ b ∈ PNat ->
   Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
@@ -1666,4 +1701,4 @@ Qed.
 
 #[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv
   SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2
-  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem.
+  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong SE_PairExt SE_FunExt : sem.
diff --git a/theories/preservation.v b/theories/preservation.v
index c8a2106..301553e 100644
--- a/theories/preservation.v
+++ b/theories/preservation.v
@@ -1,80 +1,9 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Lemma App_Inv Γ (b a : PTm) U :
-  Γ ⊢ PApp b a ∈ U ->
-  exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
-Proof.
-  move E : (PApp b a) => u hu.
-  move : b a E. elim : Γ u U / hu => //=.
-  - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
-    exists A,B.
-    repeat split => //=.
-    have [i] : exists i, Γ ⊢ PBind PPi A B ∈  PUniv i by sfirstorder use:regularity.
-    hauto lq:on use:bind_inst, E_Refl.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Abs_Inv Γ (a : PTm) U :
-  Γ ⊢ PAbs a ∈ U ->
-  exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
-Proof.
-  move E : (PAbs a) => u hu.
-  move : a E. elim : Γ u U / hu => //=.
-  - move => Γ a A B i hP _ ha _ a0 [*]. subst.
-    exists A, B. repeat split => //=.
-    hauto lq:on use:E_Refl, Su_Eq.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Proj1_Inv Γ (a : PTm ) U :
-  Γ ⊢ PProj PL a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
-Proof.
-  move E : (PProj PL a) => u hu.
-  move :a E. elim : Γ u U / hu => //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    eapply regularity in ha.
-    move : ha => [i].
-    move /Bind_Inv => [j][h _].
-    by move /E_Refl /Su_Eq in h.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Proj2_Inv Γ (a : PTm) U :
-  Γ ⊢ PProj PR a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
-Proof.
-  move E : (PProj PR a) => u hu.
-  move :a E. elim : Γ u U / hu => //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    have ha' := ha.
-    eapply regularity in ha.
-    move : ha => [i ha].
-    move /T_Proj1 in ha'.
-    apply : bind_inst; eauto.
-    apply : E_Refl ha'.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Pair_Inv Γ (a b : PTm ) U :
-  Γ ⊢ PPair a b ∈ U ->
-  exists A B, Γ ⊢ a ∈ A /\
-         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
-         Γ ⊢ PBind PSig A B ≲ U.
-Proof.
-  move E : (PPair a b) => u hu.
-  move : a b E. elim : Γ u U / hu => //=.
-  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
-    exists A,B. repeat split => //=.
-    move /E_Refl /Su_Eq : hS. apply.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
 
 Lemma Ind_Inv Γ P (a : PTm) b c U :
   Γ ⊢ PInd P a b c ∈ U ->
@@ -93,36 +22,58 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
-  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+Lemma E_Abs Γ a b A B :
+  A :: Γ ⊢ a ≡ b ∈ B ->
+  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
 Proof.
-  move => a b Γ A ha.
-  move /App_Inv : ha.
-  move => [A0][B0][ha][hb]hS.
-  move /Abs_Inv : ha => [A1][B1][ha]hS0.
-  have hb' := hb.
-  move /E_Refl in hb.
-  have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
-  have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
-  move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
-  move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
   move => h.
-  apply : E_Conv; eauto.
-  apply : E_AppAbs; eauto.
-  eauto using T_Conv.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff.
+  have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity.
+  have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
+  have hΓ' : ⊢ A::Γ by eauto with wt.
+  set k := max i j.
+  have [? ?] : i <= k /\ j <= k by lia.
+  have {}hA : Γ ⊢ A ∈ PUniv k by hauto l:on use:T_Conv, Su_Univ.
+  have {}hB : A :: Γ ⊢ B ∈ PUniv k by hauto lq:on use:T_Conv, Su_Univ.
+  have hPi : Γ ⊢ PBind PPi A B ∈ PUniv k by eauto with wt.
+  apply : E_FunExt; eauto with wt.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  apply : E_Transitive => /=. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  apply /E_Symmetric /E_Transitive. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  asimpl. rewrite !subst_scons_id. by apply E_Symmetric.
 Qed.
 
-Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
-    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Lemma E_Pair Γ a0 b0 a1 b1 A B i :
+  Γ ⊢ PBind PSig A B ∈ PUniv i ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
+  Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B.
 Proof.
-  move => a b Γ A.
-  move /Proj1_Inv. move => [A0][B0][hab]hA0.
-  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
-  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
-  move /Su_Sig_Proj1 in hS.
-  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
-  apply : E_Conv; eauto.
-  apply : E_ProjPair1; eauto.
+  move => hSig ha hb.
+  have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity.
+  have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\
+                     Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity.
+  have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt.
+  have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac].
+  apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl.
+  have ea : Γ ⊢ PProj PL (PPair a0 b0) ≡ a0 ∈ A by eauto with wt.
+  have : Γ ⊢ PProj PR (PPair a0 b0) ≡ b0 ∈ subst_PTm (scons a0 VarPTm) B by eauto with wt.
+  have : Γ ⊢ PProj PL (PPair a1 b1) ≡ a1 ∈ A by eauto using E_ProjPair1 with wt.
+  have : Γ ⊢ PProj PR (PPair a1 b1) ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B.
+  apply : E_Conv; eauto using E_ProjPair2 with wt.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto using E_Symmetric.
+  move => *.
+  apply : E_PairExt; eauto using E_Symmetric, E_Transitive.
+  apply : E_Conv. by eauto using E_Symmetric, E_Transitive.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. by eauto. apply /E_Symmetric /E_Transitive.
+  by eauto using E_ProjPair1.
+  eauto.
 Qed.
 
 Lemma Suc_Inv Γ (a : PTm) A :
@@ -159,7 +110,7 @@ Proof.
         apply : Su_Sig_Proj2; eauto.
       move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
       move {hS}.
-      move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
+      move => ?. apply : E_Conv; eauto. apply : typing.E_ProjPair2; eauto.
   - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
   - move => P a b c Γ A.
     move /Ind_Inv.
diff --git a/theories/soundness.v b/theories/soundness.v
index 7f86852..877e3fb 100644
--- a/theories/soundness.v
+++ b/theories/soundness.v
@@ -7,7 +7,7 @@ Theorem fundamental_theorem :
   (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
   (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
   (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
-  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
+  apply wt_mutual; eauto with sem.
   Unshelve. all : exact 0.
 Qed.
 
diff --git a/theories/structural.v b/theories/structural.v
index ccb4c6f..207447d 100644
--- a/theories/structural.v
+++ b/theories/structural.v
@@ -137,12 +137,12 @@ Lemma E_ProjPair2' Γ (a b : PTm) A B i U :
   Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U.
 Proof. move => ->. apply E_ProjPair2. Qed.
 
-Lemma E_AppEta' Γ (b : PTm ) A B i u :
-  u = (PApp (ren_PTm shift b) (VarPTm var_zero)) ->
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B.
-Proof. qauto l:on use:wff_mutual, E_AppEta. Qed.
+(* Lemma E_AppEta' Γ (b : PTm ) A B i u : *)
+(*   u = (PApp (ren_PTm shift b) (VarPTm var_zero)) -> *)
+(*   Γ ⊢ PBind PPi A B ∈ (PUniv i) -> *)
+(*   Γ ⊢ b ∈ PBind PPi A B -> *)
+(*   Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B. *)
+(* Proof. qauto l:on use:wff_mutual, E_AppEta. Qed. *)
 
 Lemma Su_Pi_Proj2' Γ (a0 a1 A0 A1 : PTm ) B0 B1 U T :
   U = subst_PTm (scons a0 VarPTm) B0 ->
@@ -222,17 +222,7 @@ Proof.
   - hauto lq:on ctrs:Wt,LEq.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
-  - move => Γ a b A B i hPi ihPi ha iha Δ ξ hΔ hξ.
-    move : ihPi (hΔ) (hξ). repeat move/[apply].
-    move => /Bind_Inv [j][h0][h1]h2.
-    have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
-    move {hPi}.
-    apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up.
   - move => *. apply : E_App'; eauto. by asimpl.
-  - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ξ hΔ hξ.
-    apply : E_Pair; eauto.
-    move : ihb hΔ hξ. repeat move/[apply].
-    by asimpl.
   - move => *. apply : E_Proj2'; eauto. by asimpl.
   - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
     move => Δ ξ hΔ hξ [:hP' hren].
@@ -302,9 +292,12 @@ Proof.
     move /(_ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
     move /(_ ltac:(by eauto using renaming_up)).
     by asimpl.
-  - move => *.
-    apply : E_AppEta'; eauto. by asimpl.
-  - qauto l:on use:E_PairEta.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ.
+    apply : E_FunExt; eauto. move : ihe1. asimpl. apply.
+    hfcrush use:Bind_Inv.
+    by apply renaming_up.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ.
+    apply : E_PairExt; eauto. move : ihR. asimpl. by apply.
   - hauto lq:on ctrs:LEq.
   - qauto l:on ctrs:LEq.
   - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
@@ -447,17 +440,7 @@ Proof.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
-  - move => Γ a b A B i hPi ihPi ha iha Δ ρ hΔ hρ.
-    move : ihPi (hΔ) (hρ). repeat move/[apply].
-    move => /Bind_Inv [j][h0][h1]h2.
-    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
-    move {hPi}.
-    apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up.
   - move => *. apply : E_App'; eauto. by asimpl.
-  - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ρ hΔ hρ.
-    apply : E_Pair; eauto.
-    move : ihb hΔ hρ. repeat move/[apply].
-    by asimpl.
   - hauto q:on ctrs:Eq.
   - move => *. apply : E_Proj2'; eauto. by asimpl.
   - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
@@ -524,9 +507,14 @@ Proof.
     move /(_ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
     move /(_ ltac:(sauto l:on use:morphing_up)).
     asimpl. substify. by asimpl.
-  - move => *.
-    apply : E_AppEta'; eauto. by asimpl.
-  - qauto l:on use:E_PairEta.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ.
+    move  : ihPi (hΔ) (hξ); repeat move/[apply]. move /[dup] /Bind_Inv => ihPi ?.
+    decompose [and ex] ihPi.
+    apply : E_FunExt; eauto. move : ihe1. asimpl. apply.
+    by eauto with wt.
+    by eauto using morphing_up with wt.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ.
+    apply : E_PairExt; eauto. move : ihR. asimpl. by apply.
   - hauto lq:on ctrs:LEq.
   - qauto l:on ctrs:LEq.
   - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
@@ -667,7 +655,6 @@ Proof.
     sfirstorder.
     apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
     hauto lq:on.
-  - hauto lq:on ctrs:Wt,Eq.
   - move => n i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]]
              ha [iha0 [iha1 [i1 iha2]]].
     repeat split.
@@ -677,7 +664,6 @@ Proof.
     move /E_Symmetric in ha.
     by eauto using bind_inst.
     hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt.
-  - hauto lq:on use:bind_inst db:wt.
   - hauto lq:on use:Bind_Inv db:wt.
   - move => Γ i a b A B hS _ hab [iha][ihb][j]ihs.
     repeat split => //=; eauto with wt.
@@ -726,15 +712,6 @@ Proof.
     subst Ξ.
     move : morphing_wt hc; repeat move/[apply]. asimpl. by apply.
     sauto lq:on use:substing_wt.
-  - move => Γ b A B i hP _ hb [i0 ihb].
-    repeat split => //=; eauto with wt.
-    have {}hb : (cons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B)
-                        by hauto lq:on use:weakening_wt, Bind_Inv.
-    apply : T_Abs; eauto.
-    apply : T_App'; eauto; rewrite-/ren_PTm. asimpl. by rewrite subst_scons_id.
-    apply T_Var. sfirstorder use:wff_mutual.
-    apply here.
-  - hauto lq:on ctrs:Wt.
   - move => Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
     have ? : ⊢ Γ by sfirstorder use:wff_mutual.
     exists (max i j).
diff --git a/theories/termination.v b/theories/termination.v
index 8afe24e..c5bc37e 100644
--- a/theories/termination.v
+++ b/theories/termination.v
@@ -3,280 +3,3 @@ From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 From stdpp Require Import relations (nsteps (..), rtc(..)).
 Import Psatz.
-
-Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a.
-Proof. case : a; case : b => //=. Qed.
-
-#[export]Hint Constructors algo_dom algo_dom_r : adom.
-
-Lemma algo_dom_r_inv a b :
-  algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
-Proof.
-  induction 1; hauto lq:on ctrs:rtc.
-Qed.
-
-Lemma A_HRedsL a a' b :
-  rtc HRed.R a a' ->
-  algo_dom_r a' b ->
-  algo_dom_r a b.
-  induction 1; sfirstorder use:A_HRedL.
-Qed.
-
-Lemma A_HRedsR a b b' :
-  HRed.nf a ->
-  rtc HRed.R b b' ->
-  algo_dom a b' ->
-  algo_dom_r a b.
-Proof. induction 2; sauto. Qed.
-
-Lemma algo_dom_sym :
-  (forall a b (h : algo_dom a b), algo_dom b a) /\
-    (forall a b (h : algo_dom_r a b), algo_dom_r b a).
-Proof.
-  apply algo_dom_mutual; try qauto use:tm_conf_sym db:adom.
-  move => a a' b hr h ih.
-  move /algo_dom_r_inv : ih => [a0][b0][ih0][ih1]ih2.
-  have nfa0 : HRed.nf a0 by sfirstorder use:algo_dom_no_hred.
-  sauto use:A_HRedsL, A_HRedsR.
-Qed.
-
-Definition term_metric k (a b : PTm) :=
-  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
-
-Lemma term_metric_sym k (a b : PTm) :
-  term_metric k a b -> term_metric k b a.
-Proof. hauto lq:on unfold:term_metric solve+:lia. Qed.
-
-Lemma term_metric_case k (a b : PTm) :
-  term_metric k a b ->
-  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k.
-Proof.
-  move=>[i][j][va][vb][h0] [h1][h2][h3]h4.
-  case : a h0 => //=; try firstorder.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
-    + sfirstorder qb:on use:ne_hne.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia.
-    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
-  - inversion h0 as [|A B C D E F]; subst.
-    hauto qb:on use:ne_hne.
-    inversion E; subst => /=.
-    + hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
-    + sfirstorder use:ne_hne.
-    + sfirstorder use:ne_hne.
-Qed.
-
-Lemma A_Conf' a b :
-  ishf a \/ ishne a ->
-  ishf b \/ ishne b ->
-  tm_conf a b ->
-  algo_dom_r a b.
-Proof.
-  move => ha hb.
-  have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
-  have {}hb : HRed.nf b by sfirstorder use:hf_no_hred, hne_no_hred.
-  move => ?.
-  apply A_NfNf.
-  by apply A_Conf.
-Qed.
-
-Lemma term_metric_abs : forall k a b,
-    term_metric k (PAbs a) (PAbs b) ->
-    exists k', k' < k /\ term_metric k' a b.
-Proof.
-  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
-  apply lored_nsteps_abs_inv in hva, hvb.
-  move : hva => [a'][hva]?. subst.
-  move : hvb => [b'][hvb]?. subst.
-  simpl in *. exists (k - 1).
-  hauto lq:on unfold:term_metric solve+:lia.
-Qed.
-
-Lemma term_metric_pair : forall k a0 b0 a1 b1,
-    term_metric k (PPair a0 b0) (PPair a1 b1) ->
-    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
-Proof.
-  move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
-  apply lored_nsteps_pair_inv in hva, hvb.
-  decompose record hva => {hva}.
-  decompose record hvb => {hvb}. subst.
-  simpl in *. exists (k - 1).
-  hauto lqb:on solve+:lia.
-Qed.
-
-Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1,
-    term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) ->
-    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
-Proof.
-  move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
-  apply lored_nsteps_bind_inv in hva, hvb.
-  decompose record hva => {hva}.
-  decompose record hvb => {hvb}. subst.
-  simpl in *. exists (k - 1).
-  hauto lqb:on solve+:lia.
-Qed.
-
-Lemma term_metric_suc : forall k a b,
-    term_metric k (PSuc a) (PSuc b) ->
-    exists k', k' < k /\ term_metric k' a b.
-Proof.
-  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
-  apply lored_nsteps_suc_inv in hva, hvb.
-  move : hva => [a'][hva]?. subst.
-  move : hvb => [b'][hvb]?. subst.
-  simpl in *. exists (k - 1).
-  hauto lq:on unfold:term_metric solve+:lia.
-Qed.
-
-Lemma term_metric_abs_neu k (a0 : PTm) u :
-  term_metric k (PAbs a0) u ->
-  ishne u ->
-  exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)).
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
-  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
-  move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst.
-  exists (k - 1).
-  simpl in *. split. lia.
-  exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)).
-  repeat split => //=.
-  apply lored_nsteps_app_cong.
-  by apply lored_nsteps_renaming.
-  by rewrite ishne_ren.
-  rewrite Bool.andb_true_r.
-  sfirstorder use:ne_nf_ren.
-  rewrite size_PTm_ren. lia.
-Qed.
-
-Lemma term_metric_pair_neu k (a0 b0 : PTm) u :
-  term_metric k (PPair a0 b0) u ->
-  ishne u ->
-  exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
-  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
-  move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst.
-  exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia.
-Qed.
-
-Lemma term_metric_app k (a0 b0 a1 b1 : PTm) :
-  term_metric k (PApp a0 b0) (PApp a1 b1) ->
-  ishne a0 ->
-  ishne a1 ->
-  exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3]h4.
-  move => hne0 hne1.
-  move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply].
-  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
-  move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply].
-  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
-  simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia.
-Qed.
-
-Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) :
-  term_metric k (PProj p0 a0) (PProj p1 a1) ->
-  ishne a0 ->
-  ishne a1 ->
-  exists j, j < k /\ term_metric j a0 a1.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
-  move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
-  move => [i0][a2][hi][?]ha02. subst.
-  move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
-  move => [i1][a3][hj][?]ha13. subst.
-  exists (k- 1).  hauto q:on use:ne_nf solve+:lia.
-Qed.
-
-Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 :
-  term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
-  ishne a0 ->
-  ishne a1 ->
-  exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\
-         term_metric j b0 b1 /\ term_metric j c0 c1.
-Proof.
-  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
-  move /lored_nsteps_ind_inv /(_ hne0) : h0.
-  move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
-  move /lored_nsteps_ind_inv /(_ hne1) : h1.
-  move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
-  exists (k -1). simpl in *.
-  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
-Qed.
-
-
-Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b.
-Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed.
-
-Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
-Proof.
-  move => [:hneL].
-  elim /Wf_nat.lt_wf_ind.
-  move => n ih a b h.
-  case /term_metric_case : (h); cycle 1.
-  move => [k'][a'][h0][h1]h2.
-  by apply : A_HRedL; eauto.
-  case /term_metric_sym /term_metric_case : (h); cycle 1.
-  move => [k'][b'][hb][/term_metric_sym h0]h1.
-  move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
-  by apply : A_HRedR; eauto.
-  move => /[swap].
-  case => hfa; case => hfb.
-  - move : hfa hfb h.
-    case : a; case : b => //=; eauto 5 using A_Conf' with adom.
-    + hauto lq:on use:term_metric_abs db:adom.
-    + hauto lq:on use:term_metric_pair db:adom.
-    + hauto lq:on use:term_metric_bind db:adom.
-    + hauto lq:on use:term_metric_suc db:adom.
-  - abstract : hneL n ih a b h hfa hfb.
-    case : a hfa h => //=.
-    + hauto lq:on use:term_metric_abs_neu db:adom.
-    + scrush use:term_metric_pair_neu db:adom.
-    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
-    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
-    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
-    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
-    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
-  - hauto q:on use:algo_dom_sym, term_metric_sym.
-  - move {hneL}.
-    case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom.
-    + move => a0 b0 a1 b1 nfa0 nfa1.
-      move /term_metric_app /(_ nfa0  nfa1) => [j][hj][ha]hb.
-      apply A_NfNf. apply A_AppCong => //; eauto.
-      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
-      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
-      eauto using algo_dom_r_algo_dom.
-    + move => p0 A0 p1 A1 neA0 neA1.
-      have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred.
-      have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred.
-      hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom.
-    + move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1.
-      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
-      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
-      hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
-Qed.
-
-Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b.
-Proof.
-  move /LoReds.FromSN => [va [ha0 ha1]].
-  move /LoReds.FromSN => [vb [hb0 hb1]].
-  eapply relations.rtc_nsteps in ha0.
-  eapply relations.rtc_nsteps in hb0.
-  hauto lq:on unfold:term_metric solve+:lia.
-Qed.
-
-Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b.
-Proof.
-  move : sn_term_metric; repeat move/[apply].
-  move => [k]+.
-  eauto using term_metric_algo_dom.
-Qed.
diff --git a/theories/typing.v b/theories/typing.v
index ae78747..e911d51 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -89,23 +89,12 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
   (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
 
-| E_Abs Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  (cons A Γ) ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
-
 | E_App Γ i (b0 b1 a0 a1 : PTm) A B :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
 
-| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a0 ≡ a1 ∈ A ->
-  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
-  Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
-
 | E_Proj1 Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
@@ -164,16 +153,20 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
   (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
   Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
 
-(* Eta *)
-| E_AppEta Γ (b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+| E_FunExt Γ (a b : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ a ∈ PBind PPi A B ->
   Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B
 
-| E_PairEta Γ (a : PTm ) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+| E_PairExt Γ (a b : PTm) A B i :
+  Γ ⊢ PBind PSig A B ∈ PUniv i ->
   Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B
 
 with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
@@ -242,10 +235,3 @@ Scheme wf_ind := Induction for Wff Sort Prop
   with le_ind := Induction for LEq Sort Prop.
 
 Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.
-
-(* Lemma lem : *)
-(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
-(*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
-(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *)
-(*   (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *)
-(* Proof. apply wt_mutual. ... *)