Prove PairEta

Add renaming_comp
Add E_AppEta
2025-04-19 00:24:09 -04:00 · 2025-04-19 00:07:48 -04:00 · 2025-04-18 16:38:34 -04:00 · 2025-04-18 15:46:07 -04:00 · 2025-04-18 15:42:40 -04:00 · 2025-04-18 14:13:46 -04:00
12 changed files with 1691 additions and 1927 deletions
--- 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.
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
--- 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.
--- 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.
--- 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.
+    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.
-    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.
+  - 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.
-      sfirstorder use:coqleq_no_hred.
-      have ? : b' = y by eauto using hred_deter. subst.
-      sauto lq:on.
+    + have ? : HRed.nf b'0 by hauto l:on use:coqleq_no_hred.
+      sfirstorder unfold:HRed.nf.
+    + sauto lq:on use:hred_deter.
 Qed.
--- 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 :
--- 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.
--- 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.
--- 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.

--- 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).
--- 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.
--- 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. ... *)
Author	SHA1	Message	Date
Yiyun Liu	0e04a7076b	Prove PairEta	2025-04-19 00:24:09 -04:00
Yiyun Liu	8e083aad4b	Add renaming_comp	2025-04-19 00:07:48 -04:00
Yiyun Liu	2b92845e3e	Add E_AppEta	2025-04-18 16:38:34 -04:00
Yiyun Liu	43daff1b27	Fix soundness	2025-04-18 15:46:07 -04:00
Yiyun Liu	d9282fb815	Finish preservation	2025-04-18 15:42:40 -04:00
Yiyun Liu	87b84794b4	Fix structural rules	2025-04-18 14:13:46 -04:00
Yiyun Liu	7c985fa58e	Minor	2025-04-17 16:42:57 -04:00
Yiyun Liu	e1fc6b609d	Add the extensional representation of pair&abs equality rules	2025-04-17 15:22:45 -04:00
Yiyun Liu	a367591e9a	Add extensional version of pair equality rules	2025-04-17 15:15:58 -04:00
Yiyun Liu	ef8feb63c3	Redefine semantic context well-formedness as an inductive	2025-04-17 15:07:14 -04:00
Yiyun Liu	4b2bbeea6f	Add SE_FunExt	2025-04-16 23:57:00 -04:00
Yiyun Liu	f9d3a620f4	Remove itauto dependency as it introduces weird axioms	2025-03-11 16:27:31 -04:00
Yiyun Liu	8dbef3e29e	Finish refactoring	2025-03-11 16:24:57 -04:00
Yiyun Liu	96ad0a4740	Add stub for the new coqleq_complete'	2025-03-11 00:14:43 -04:00
Yiyun Liu	181e06ae01	Finish the completeness proof for equality	2025-03-10 23:45:19 -04:00
Yiyun Liu	9d68e5d6c9	Finish the conf case	2025-03-10 23:22:09 -04:00
Yiyun Liu	d1771adc48	Use hne and hf instead HRed.nf	2025-03-10 22:44:42 -04:00
Yiyun Liu	30caf75002	Make progress on the refactored lemma	2025-03-10 19:58:19 -04:00
Yiyun Liu	030dccb326	Finish the refactored executable_correct	2025-03-10 19:02:51 -04:00
Yiyun Liu	4021d05d99	Update executable to use salgo_dom for subtyping	2025-03-10 18:18:42 -04:00
Yiyun Liu	e278c6eaef	Define salgo_dom	2025-03-10 16:22:37 -04:00
Yiyun Liu	4cbd2ac0fd	Save	2025-03-10 15:35:43 -04:00
Yiyun Liu	849d19708e	Add new definition of algo_dom	2025-03-10 14:30:36 -04:00