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
15 changed files with 3496 additions and 3019 deletions
--- a/2
+++ b/2
@ -22,6 +22,6 @@ theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fint
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v theories/Autosubst2/unscoped.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
 FORCE:
--- a/syntax.sig
+++ b/syntax.sig
@ -16,7 +16,6 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
 PBot : PTm
 PNat : PTm
 PZero : PTm
 PSuc : PTm -> PTm
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@ -41,7 +41,6 @@ Inductive PTm : Type :=
  | PProj : PTag -> PTm -> PTm
  | PBind : BTag -> PTm -> PTm -> PTm
  | PUniv : nat -> PTm
  | PBot : PTm
  | PNat : PTm
  | PZero : PTm
  | PSuc : PTm -> PTm
@ -88,11 +87,6 @@ Proof.
 exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)).
 Qed.
 Lemma congr_PBot : PBot = PBot.
 Proof.
 exact (eq_refl).
 Qed.
 Lemma congr_PNat : PNat = PNat.
 Proof.
 exact (eq_refl).
@ -135,7 +129,6 @@ Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
  | PBind s0 s1 s2 =>
      PBind s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2)
  | PUniv s0 => PUniv s0
  | PBot => PBot
  | PNat => PNat
  | PZero => PZero
  | PSuc s0 => PSuc (ren_PTm xi_PTm s0)
@ -160,7 +153,6 @@ Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
  | PBind s0 s1 s2 =>
      PBind s0 (subst_PTm sigma_PTm s1) (subst_PTm (up_PTm_PTm sigma_PTm) s2)
  | PUniv s0 => PUniv s0
  | PBot => PBot
  | PNat => PNat
  | PZero => PZero
  | PSuc s0 => PSuc (subst_PTm sigma_PTm s0)
@ -199,7 +191,6 @@ subst_PTm sigma_PTm s = s :=
      congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
        (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0)
@ -243,7 +234,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
        (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upExtRen_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
@ -291,7 +281,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
        (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (upExt_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
@ -339,7 +328,6 @@ Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
        (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 => congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
@ -392,7 +380,6 @@ Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
        (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 =>
@ -458,7 +445,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
        (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 =>
@ -525,7 +511,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
        (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 =>
@ -634,7 +619,6 @@ Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
        (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
           (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv s0 => congr_PUniv (eq_refl s0)
  | PBot => congr_PBot
  | PNat => congr_PNat
  | PZero => congr_PZero
  | PSuc s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
--- a/theories/admissible.v
+++ b/theories/admissible.v
@ -1,45 +1,88 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
-Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
+Derive Inversion wff_inv with (forall Γ, ⊢ Γ) Sort Prop.
-Lemma Wff_Cons_Inv n Γ (A : PTm n) :
+Lemma T_Abs Γ (a : PTm ) A B :
-  ⊢ funcomp (ren_PTm shift) (scons A Γ) ->
+  (cons A Γ) ⊢ a ∈ B ->
  ⊢ Γ /\ exists i, Γ ⊢ A ∈ PUniv i.
 Proof.
  elim /wff_inv => //= _.
  move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
  Equality.simplify_dep_elim.
  have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
  move /(_ var_zero) : (h).
  rewrite /funcomp. asimpl.
  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
  move => ?. subst.
  have : Γ0 = Γ. extensionality i.
  move /(_ (Some i)) : h.
  rewrite /funcomp. asimpl.
  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
  done.
  move => ?. subst. sfirstorder.
 Qed.
 Lemma T_Abs n Γ (a : PTm (S n)) A B :
  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
  Γ ⊢ PAbs a ∈ PBind PPi A B.
 Proof.
  move => ha.
-  have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have [i hB] : exists i, (cons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
-  have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
+  have hΓ : ⊢  (cons A Γ) by sfirstorder use:wff_mutual.
-  move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
+  hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
  hauto lq:on rew:off use:T_Bind', typing.T_Abs.
 Qed.
-Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+
 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 ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
 Proof.
  move => h0 h1.
@ -49,7 +92,7 @@ Proof.
  firstorder.
 Qed.
-Lemma E_App n Γ (b0 b1 a0 a1 : PTm n) A B :
+Lemma E_App Γ (b0 b1 a0 a1 : PTm ) A B :
  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
  Γ ⊢ a0 ≡ a1 ∈ A ->
  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
@ -59,7 +102,7 @@ Proof.
  move : E_App h. by repeat move/[apply].
 Qed.
-Lemma E_Proj2 n Γ (a b : PTm n) A B :
+Lemma E_Proj2 Γ (a b : PTm) A B :
  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
 Proof.
@ -67,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,42 +1,71 @@
-Require Import Autosubst2.fintype 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.
 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)
 | there i Γ A B :
  lookup i Γ A ->
  lookup (S i) (cons B Γ) (ren_PTm shift A).
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+Lemma lookup_deter i Γ A B :
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
+  lookup i Γ A ->
  lookup i Γ B ->
  A = B.
 Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed.
-Lemma up_injective n m (ξ : fin n -> fin m) :
+Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
-  (forall i j, ξ i = ξ j -> i = j) ->
+Proof.  move => ->. apply here. Qed.
-  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+
 Lemma there' i Γ A B U : U = ren_PTm shift A -> lookup i Γ A ->
                       lookup (S i) (cons B Γ) U.
 Proof. move => ->. apply there. Qed.
 Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A).
 Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=
  forall i A, lookup i Δ A -> lookup (ξ i) Γ (ren_PTm ξ A).
 Definition ren_inj (ξ : nat -> nat) := forall i j, ξ i = ξ j -> i = j.
 Lemma up_injective (ξ : nat -> nat) :
  ren_inj ξ ->
  ren_inj (upRen_PTm_PTm ξ).
 Proof.
-  sblast inv:option.
+  move => h i j.
  case : i => //=; case : j => //=.
  move => i j. rewrite /funcomp. hauto lq:on rew:off unfold:ren_inj.
 Qed.
 Local Ltac2 rec solve_anti_ren () :=
  let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
  intro $x;
  lazy_match! Constr.type (Control.hyp x) with
-  | fin _ -> _ _ => (ltac1:(case;hauto lq:on rew:off use:up_injective))
+  | nat -> nat => (ltac1:(case => *//=; qauto l:on use:up_injective unfold:ren_inj))
  | _ => solve_anti_ren ()
  end.
 Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
-Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+Lemma ren_injective (a b : PTm) (ξ : nat -> nat) :
-  (forall i j, ξ i = ξ j -> i = j) ->
+  ren_inj ξ ->
  ren_PTm ξ a = ren_PTm ξ b ->
  a = b.
 Proof.
-  move : m ξ b. elim : n / a => //; try solve_anti_ren.
+  move : ξ b. elim : a => //; try solve_anti_ren.
  move => p ihp ξ []//=. hauto lq:on inv:PTm, nat ctrs:- use:up_injective.
 Qed.
 Inductive HF : Set :=
 | H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
-Definition ishf {n} (a : PTm n) :=
+Definition ishf (a : PTm) :=
  match a with
  | PPair _ _ => true
  | PAbs _ => true
@ -48,7 +77,7 @@ Definition ishf {n} (a : PTm n) :=
  | _ => false
  end.
-Definition toHF {n} (a : PTm n) :=
+Definition toHF (a : PTm) :=
  match a with
  | PPair _ _ => H_Pair
  | PAbs _ => H_Abs
@ -60,54 +89,513 @@ Definition toHF {n} (a : PTm n) :=
  | _ => H_Bot
  end.
-Fixpoint ishne {n} (a : PTm n) :=
+Fixpoint ishne (a : PTm) :=
  match a with
  | VarPTm _ => true
  | PApp a _ => ishne a
  | PProj _ a => ishne a
  | PBot => true
  | PInd _ n _ _ => ishne n
  | _ => false
  end.
-Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
+Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false.
-Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
+Definition isuniv (a : PTm) := if a is PUniv _ then true else false.
-Definition ispair {n} (a : PTm n) :=
+Definition ispair (a : PTm) :=
  match a with
  | PPair _ _ => true
  | _ => false
  end.
-Definition isnat {n} (a : PTm n) := if a is PNat then true else false.
+Definition isnat (a : PTm) := if a is PNat then true else false.
-Definition iszero {n} (a : PTm n) := if a is PZero then true else false.
+Definition iszero (a : PTm) := if a is PZero then true else false.
-Definition issuc {n} (a : PTm n) := if a is PSuc _ then true else false.
+Definition issuc (a : PTm) := if a is PSuc _ then true else false.
-Definition isabs {n} (a : PTm n) :=
+Definition isabs (a : PTm) :=
  match a with
  | PAbs _ => true
  | _ => false
  end.
-Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+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.
-Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition isabs_ren (a : PTm)  (ξ : nat -> nat) :
  isabs (ren_PTm ξ a) = isabs a.
 Proof. case : a => //=. Qed.
-Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ispair_ren (a : PTm)  (ξ : nat -> nat) :
  ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
-Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+Definition ishne_ren (a : PTm)  (ξ : nat -> nat) :
  ishne (ren_PTm ξ a) = ishne a.
-Proof. move : m ξ. elim : n / a => //=. Qed.
+Proof. move : ξ. elim : a => //=. Qed.
-Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A :
+Lemma renaming_shift Γ A :
-  renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift.
+  renaming_ok (cons A Γ) Γ shift.
-Proof. sfirstorder. Qed.
+Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed.
 Lemma subst_scons_id (a : PTm) :
  subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) a = a.
 Proof.
  have E : subst_PTm VarPTm a = a by asimpl.
  rewrite -{2}E.
  apply ext_PTm. case => //=.
 Qed.
 Module HRed.
    Inductive R : PTm -> PTm ->  Prop :=
  (****************** Beta ***********************)
  | AppAbs a b :
    R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
  | ProjPair p a b :
    R (PProj p (PPair a b)) (if p is PL then a else b)
  | IndZero P b c :
    R (PInd P PZero b c) b
  | IndSuc P a b c :
    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
  (*************** Congruence ********************)
  | AppCong a0 a1 b :
    R a0 a1 ->
    R (PApp a0 b) (PApp a1 b)
  | ProjCong p a0 a1 :
    R a0 a1 ->
    R (PProj p a0) (PProj p a1)
  | IndCong P a0 a1 b c :
    R a0 a1 ->
    R (PInd P a0 b c) (PInd P a1 b c).
    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
@ -1,344 +1,29 @@
 From Equations Require Import Equations.
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
-Derive NoConfusion for option sig nat PTag BTag PTm.
+Require Import Logic.PropExtensionality (propositional_extensionality).
-Derive EqDec for BTag PTag PTm.
+Require Import ssreflect ssrbool.
 Import Logic (inspect).
-Require Import Cdcl.Itauto.
+From Ltac2 Require Import Ltac2.
 Import Ltac2.Constr.
 Set Default Proof Mode "Classic".
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
-Definition ishf (a : PTm) :=
+Ltac2 destruct_algo () :=
-  match a with
+  lazy_match! goal with
-  | PPair _ _ => true
+  | [h : algo_dom ?a ?b |- _ ] =>
-  | PAbs _ => true
+      if is_var a then destruct $a; ltac1:(done)  else
-  | PUniv _ => true
+        (if is_var b then destruct $b; ltac1:(done) else ())
  | PBind _ _ _ => true
  | PNat => true
  | PSuc _ => true
  | PZero => true
  | _ => false
  end.
 Fixpoint ishne (a : PTm) :=
  match a with
  | VarPTm _ => true
  | PApp a _ => ishne a
  | PProj _ a => ishne a
  | PBot => true
  | PInd _ n _ _ => ishne n
  | _ => false
  end.
 Module HRed.
  Inductive R : PTm -> PTm ->  Prop :=
  (****************** Beta ***********************)
  | AppAbs a b :
    R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
  | ProjPair p a b :
    R (PProj p (PPair a b)) (if p is PL then a else b)
  | IndZero P b c :
    R (PInd P PZero b c) b
  | IndSuc P a b c :
    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
  (*************** Congruence ********************)
  | AppCong a0 a1 b :
    R a0 a1 ->
    R (PApp a0 b) (PApp a1 b)
  | ProjCong p a0 a1 :
    R a0 a1 ->
    R (PProj p a0) (PProj p a1)
  | IndCong P a0 a1 b c :
    R a0 a1 ->
    R (PInd P a0 b c) (PInd P a1 b c).
  Definition nf a := forall b, ~ R a b.
 End HRed.
 Definition isbind  (a : PTm) := if a is PBind _ _ _ then true else false.
 Definition isuniv  (a : PTm) := if a is PUniv _ then true else false.
 Definition ispair  (a : PTm) :=
  match a with
  | PPair _ _ => true
  | _ => false
  end.
 Definition isnat  (a : PTm) := if a is PNat then true else false.
 Definition iszero  (a : PTm) := if a is PZero then true else false.
 Definition issuc  (a : PTm) := if a is PSuc _ then true else false.
 Definition isabs  (a : PTm) :=
  match a with
  | PAbs _ => true
  | _ => false
  end.
 Definition tm_nonconf (a b : PTm) : bool :=
  match a, b with
  | PAbs _, _ => ishne b || isabs b
  | _, PAbs _ => ishne a
  | VarPTm _, VarPTm _ => true
  | PPair _ _, _ => ishne b || ispair b
  | _, PPair _ _ => ishne a
  | PZero, PZero => true
  | PSuc _, PSuc _ => true
  | PApp _ _, PApp _ _ => ishne a && ishne b
  | PProj _ _, PProj _ _ => ishne a && ishne b
  | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne 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 :
  ~~ isabs b ->
  eq_view (PAbs a) b
 | V_NeuAbs a b :
  ~~ isabs 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 :
  ~~ ispair u ->
  eq_view (PPair a0 b0) u
 | V_NeuPair u a1 b1 :
  ~~ ispair 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 :
  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) b := V_AbsNeu a b _;
  tm_to_eq_view a (PAbs b) := V_NeuAbs a b _;
  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 u (PPair a1 b1) := V_NeuPair u 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)
 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'  :
  ishne a \/ ishf a ->
  HRed.R b b' ->
  algo_dom_r a b' ->
  (* ----------------------- *)
  algo_dom_r a b.
 Lemma algo_dom_hf_hne (a b : PTm) :
  algo_dom a b ->
  (ishf a \/ ishne a) /\ (ishf b \/ ishne b).
 Proof.
  induction 1 =>//=; hauto lq:on.
 Qed.
 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.
 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
    | PBot => 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.
 Ltac check_equal_triv :=
  intros;subst;
  lazymatch goal with
  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
-  | [h : algo_dom _ _ |- _] => try (inversion h; by subst)
+  | [h : algo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
  | _ => idtac
  end.
@ -349,81 +34,317 @@ Ltac solve_check_equal :=
  | _ => idtac
  end].
-Equations check_equal (a b : PTm) (h : algo_dom a b) :
+Global Set Transparent Obligations.
  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.eqb 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
-  (* check_equal a b h := false; *)
+Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
-  with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
+
-  bool by struct h0 :=
+Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
-  check_equal_r a b h with inspect (hred a) :=
+  match a, b with
-    check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _;
+  | VarPTm i, VarPTm j => nat_eqdec i j
-  check_equal_r a b h (exist _ None k) with  inspect (hred b) :=
+  | PAbs a, PAbs b => check_equal_r a b _
-    | (exist _ None l) => tm_nonconf a b && check_equal a b _;
+  | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
-    | (exist _ (Some b') l) => check_equal_r a b'  _.
+  | 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.
-  destruct h.
+  inversion h; subst => //=.
-  exfalso. apply algo_dom_hf_hne in H.
+  exfalso. sfirstorder use:algo_dom_no_hred.
-  apply hred_sound in k.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
-  destruct H as [[|] _].
+  exfalso. sfirstorder.
  eauto using hf_no_hred.
  eauto using hne_no_hred.
  apply hred_sound in k.
  assert (  a'0 = a')by eauto using hred_deter. subst.
  apply h.
  exfalso.
  apply hred_sound in k.
  destruct H as [|].
  eauto using hne_no_hred.
  eauto using hf_no_hred.
 Defined.
 Next Obligation.
-  simpl. intros.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
-  inversion h; subst =>//=.
+  destruct b' as [b' hb']. simpl.
-  move {h}. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound.
+  inversion h; subst.
-  apply False_ind. hauto l:on use:hred_complete.
+  - exfalso.
-  assert (b' = b'0) by eauto using hred_deter, hred_sound.
+    sfirstorder use:algo_dom_no_hred.
-  subst.
+  - exfalso.
-  assumption.
+    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.
-  intros.
+  move => /= a b hdom ha _ hb _.
-  inversion h; subst => //=.
+  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.
 Lemma check_equal_abs_neu a u neu h : check_equal (PAbs a) u (A_AbsNeu a u neu h) = check_equal_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) h.
 Proof. case : u neu h => //=.  Qed.
 Lemma check_equal_neu_abs a u neu h : check_equal u (PAbs a) (A_NeuAbs a u neu h) = check_equal_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a h.
 Proof. case : u neu h => //=.  Qed.
 Lemma check_equal_pair_pair a0 b0 a1 b1 a h :
  check_equal (PPair a0 b0) (PPair a1 b1) (A_PairPair a0 a1 b0 b1 a h) =
    check_equal_r a0 a1 a && check_equal_r b0 b1 h.
 Proof. reflexivity. Qed.
 Lemma check_equal_pair_neu a0 a1 u neu h h'
  : check_equal (PPair a0 a1) u (A_PairNeu a0 a1 u neu h h') = check_equal_r a0 (PProj PL u) h && check_equal_r a1 (PProj PR u) h'.
 Proof.
  case : u neu h h' => //=.
 Qed.
 Lemma check_equal_neu_pair a0 a1 u neu h h'
  : check_equal u (PPair a0 a1) (A_NeuPair a0 a1 u neu h h') = check_equal_r  (PProj PL u) a0 h && check_equal_r (PProj PR u) a1 h'.
 Proof.
  case : u neu h h' => //=.
 Qed.
 Lemma check_equal_bind_bind p0 A0 B0 p1 A1 B1 h0 h1 :
  check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) (A_BindCong p0 p1 A0 A1 B0 B1 h0 h1) =
    BTag_eqdec p0 p1 &&  check_equal_r A0 A1 h0 && check_equal_r  B0 B1 h1.
 Proof. reflexivity. Qed.
 Lemma check_equal_proj_proj p0 u0 p1 u1 neu0 neu1 h :
  check_equal (PProj p0 u0) (PProj p1 u1) (A_ProjCong p0 p1 u0 u1 neu0 neu1 h) =
    PTag_eqdec p0 p1 && check_equal u0 u1 h.
 Proof. reflexivity. Qed.
 Lemma check_equal_app_app u0 a0 u1 a1 hu0 hu1 hdom hdom' :
  check_equal (PApp u0 a0) (PApp u1 a1) (A_AppCong u0 u1 a0 a1 hu0 hu1 hdom hdom') =
    check_equal u0 u1 hdom && check_equal_r a0 a1 hdom'.
 Proof. reflexivity. Qed.
 Lemma check_equal_ind_ind P0 u0 b0 c0 P1 u1 b1 c1 neu0 neu1 domP domu domb domc :
  check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
    (A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP domu domb domc) =
    check_equal_r P0 P1 domP && check_equal u0 u1 domu && check_equal_r b0 b1 domb && check_equal_r c0 c1 domc.
 Proof. reflexivity. Qed.
 Lemma hred_none a : HRed.nf a -> hred a = None.
 Proof.
  destruct (hred a) eqn:eq;
  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.
  simp_check_r.
  destruct (fancy_hred a).
  destruct (fancy_hred b).
  reflexivity.
  exfalso. hauto l:on use:hred_complete.
  exfalso. hauto l:on use:hred_complete.
 Qed.
 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.
  destruct (fancy_hred a).
  - hauto q:on unfold:HRed.nf.
  - destruct s as [x ?].
    have ? : x = a' by eauto using hred_deter. subst.
    simpl.
    f_equal.
    apply PropExtensionality.proof_irrelevance.
 Qed.
 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.
  destruct (fancy_hred a).
  - simpl.
    destruct (fancy_hred b) as [|[b'' hb']].
    + hauto lq:on unfold:HRed.nf.
    + simpl.
      have ? : (b'' = b') by eauto using hred_deter. subst.
      f_equal.
      apply PropExtensionality.proof_irrelevance.
  - exfalso.
    sfirstorder use:hne_no_hred, hf_no_hred.
 Qed.
 Lemma check_equal_univ i j :
  check_equal (PUniv i) (PUniv j) (A_UnivCong i j) = nat_eqdec i j.
 Proof. reflexivity. Qed.
 Lemma check_equal_conf a b nfa nfb nfab :
  check_equal a b (A_Conf a b nfa nfb nfab) = false.
 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.
 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.
 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 A1 A0 _ && check_sub_r B0 B1 _
  | PBind PSig A0 B0, PBind PSig A1 B1 =>
      check_sub_r A0 A1 _ && check_sub_r B0 B1 _
  | PUniv i, PUniv j =>
      PeanoNat.Nat.leb i j
  | PNat, PNat => true
  | 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 (a b : PTm) (h : salgo_dom_r a b) {struct h} :=
  match fancy_hred a with
  | inr a' => check_sub_r (proj1_sig a') b _
  | inl ha' => match fancy_hred b with
            | 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:salgo_dom_no_hred.
  assert (a' = a'0) by eauto using hred_deter. by subst.
  exfalso. sfirstorder.
 Defined.
 Next Obligation.
-  qauto inv:algo_dom, algo_dom_r.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
  destruct b' as [b' hb']. simpl.
  inversion h; subst.
  - exfalso.
    sfirstorder use:salgo_dom_no_hred.
  - exfalso.
    sfirstorder.
  - assert (b' = b'0) by eauto using hred_deter. by subst.
 Defined.
-(* Do not step back from here or otherwise equations will cause an error *)
+
 (* 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_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 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 (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j.
 Proof. reflexivity. Qed.
 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: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)=>//=.
  destruct (fancy_hred a) =>//=.
  destruct s as [a' ha']. simpl.
  hauto l:on use:hred_complete.
  destruct s as [b' hb']. simpl.
  hauto l:on use:hred_complete.
 Qed.
 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).
  - hauto q:on unfold:HRed.nf.
  - destruct s as [x ?].
    have ? : x = a' by eauto using hred_deter. subst.
    simpl.
    f_equal.
    apply PropExtensionality.proof_irrelevance.
 Qed.
 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).
  - simpl.
    destruct (fancy_hred b) as [|[b'' hb']].
    + hauto lq:on unfold:HRed.nf.
    + simpl.
      have ? : (b'' = b') by eauto using hred_deter. subst.
      f_equal.
      apply PropExtensionality.proof_irrelevance.
  - exfalso.
    sfirstorder use:hne_no_hred, hf_no_hred.
 Qed.
 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
@ -0,0 +1,259 @@
 From Equations Require Import Equations.
 Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common executable algorithmic.
 Require Import ssreflect ssrbool.
 From stdpp Require Import relations (rtc(..)).
 From Hammer Require Import Tactics.
 Lemma coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b.
 Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed.
 Lemma coqeq_no_hred a b : a ↔ b -> HRed.nf a /\ HRed.nf b.
 Proof. induction 1;
         qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf.
 Qed.
 Lemma coqleq_no_hred a b : a ⋖ b -> HRed.nf a /\ HRed.nf b.
 Proof.
  induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred, coqeqr_no_hred unfold:HRed.nf.
 Qed.
 Lemma coqeq_neuneu u0 u1 :
  ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
 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).
 Proof.
  apply algo_dom_mutual.
  - move => a b h.
    move => h0.
    rewrite check_equal_abs_abs.
    constructor. tauto.
  - move => a u i h0 ih h.
    apply CE_AbsNeu => //.
    apply : ih. simp check_equal tm_to_eq_view in h.
    by rewrite check_equal_abs_neu in h.
  - move => a u i h ih h0.
    apply CE_NeuAbs=>//.
    apply ih.
    by rewrite check_equal_neu_abs in h0.
  - move => a0 a1 b0 b1 a ha h.
    move => h0.
    rewrite check_equal_pair_pair. move /andP => [h1 h2].
    sauto lq:on.
  - move => a0 a1 u neu h ih h' ih' he.
    rewrite check_equal_pair_neu in he.
    apply CE_PairNeu => //; hauto lqb:on.
  - move => a0 a1 u i a ha a2 hb.
    rewrite check_equal_neu_pair => *.
    apply CE_NeuPair => //; hauto lqb:on.
  - sfirstorder.
  - hauto l:on use:CE_SucSuc.
  - move => i j /sumboolP.
    hauto lq:on use:CE_UnivCong.
  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1 h2.
    rewrite check_equal_bind_bind in h2.
    move : h2.
    move /andP => [/andP [h20 h21] h3].
    move /sumboolP : h20 => ?. subst.
    hauto l:on use:CE_BindCong.
  - 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 => 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].
    sauto lq:on use:coqeq_neuneu.
  - move => a b n n0 i. by rewrite check_equal_conf.
  - move => a b dom h ih. apply : CE_HRed; eauto using rtc_refl.
    rewrite check_equal_nfnf in ih.
    tauto.
  - move => a a' b ha doma ih hE.
    rewrite check_equal_hredl in hE. sauto lq:on.
  - move => a b b' hu r a0 ha hb. rewrite check_equal_hredr in hb.
    sauto lq:on rew:off.
 Qed.
 Ltac ce_solv := move => *; simp ce_prop in *; hauto qb:on rew:off inv:CoqEq, CoqEq_Neu.
 Lemma check_equal_complete :
  (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).
 Proof.
  apply algo_dom_mutual.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - ce_solv.
  - move => i j.
    rewrite check_equal_univ.
    case : nat_eqdec => //=.
    ce_solv.
  - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1.
    rewrite check_equal_bind_bind.
    move /negP.
    move /nandP.
    case. move /nandP.
    case. move => h. have : p0 <> p1  by sauto lqb:on.
    clear. move => ?. hauto lq:on rew:off inv:CoqEq, CoqEq_Neu.
    hauto qb:on inv:CoqEq,CoqEq_Neu.
    hauto qb:on inv:CoqEq,CoqEq_Neu.
  - 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 => 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.
    inversion h; subst.
    inversion H; subst.
    move /negP /nandP.
    case. move/nandP.
    case. move/nandP.
    case. qauto b:on inv:CoqEq, CoqEq_Neu.
    sauto lqb:on inv:CoqEq, CoqEq_Neu.
    sauto lqb:on inv:CoqEq, CoqEq_Neu.
    sauto lqb:on inv:CoqEq, CoqEq_Neu.
  - rewrite /tm_conf.
    move => a b n n0 i. simp ce_prop.
    move => _. inversion 1; subst => //=.
    + destruct b => //=.
    + destruct a => //=.
    + destruct b => //=.
    + destruct a => //=.
    + hauto l:on inv:CoqEq_Neu.
  - move => a b h ih.
    rewrite check_equal_nfnf.
    move : ih => /[apply].
    move => + h0.
    have {h} [? ?] : HRed.nf a /\ HRed.nf b by sfirstorder use:algo_dom_no_hred.
    inversion h0; 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:coqeq_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_equal_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:coqeq_no_hred.
      sfirstorder unfold:HRed.nf.
    + sauto lq:on use:hred_deter.
 Qed.
 Ltac simp_sub := with_strategy opaque [check_equal] simpl in *.
 Lemma check_sub_sound :
  (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 salgo_dom_mutual; try done.
  - simpl. move => i j [];
    sauto lq:on use:Reflect.Nat_leb_le.
  - 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}.
    sauto lq:on rew:off.
 Qed.
 Lemma check_sub_complete :
  (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 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 => /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 => /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.
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
--- a/theories/logrel.v
+++ b/theories/logrel.v
--- a/theories/preservation.v
+++ b/theories/preservation.v
@ -1,91 +1,20 @@
-Require Import Autosubst2.core Autosubst2.fintype 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 n Γ (b a : PTm n) 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 : n Γ u U / hu => n //=.
  - 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 n Γ (a : PTm (S n)) U :
+Lemma Ind_Inv Γ P (a : PTm) b c U :
  Γ ⊢ PAbs a ∈ U ->
  exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
 Proof.
  move E : (PAbs a) => u hu.
  move : a E. elim : n Γ u U / hu => n //=.
  - 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 n Γ (a : PTm n) 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 : n Γ u U / hu => n //=.
  - 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 n Γ (a : PTm n) 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 : n Γ u U / hu => n //=.
  - 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 n Γ (a b : PTm n) 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 : n Γ u U / hu => n //=.
  - 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 n Γ P (a : PTm n) b c U :
  Γ ⊢ PInd P a b c ∈ U ->
-  exists i, funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i /\
+  exists i, (cons PNat Γ) ⊢ P ∈ PUniv i /\
       Γ ⊢ a ∈ PNat /\
       Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P /\
-      funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
+          (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
       Γ ⊢ subst_PTm (scons a VarPTm) P ≲ U.
 Proof.
  move E : (PInd P a b c)=> u hu.
-  move : P a b c E. elim : n Γ u U / hu => n //=.
+  move : P a b c E. elim : Γ u U / hu => //=.
  - move => Γ P a b c i hP _ ha _ hb _ hc _ P0 a0 b0 c0 [*]. subst.
    exists i. repeat split => //=.
    have : Γ ⊢ subst_PTm (scons a VarPTm) P ∈ subst_PTm (scons a VarPTm) (PUniv i) by hauto l:on use:substing_wt.
@ -93,57 +22,79 @@ Proof.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.
-Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+Lemma E_Abs Γ a b A B :
-  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+  A :: Γ ⊢ a ≡ b ∈ B ->
  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
 Proof.
  move => n 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.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff.
-  apply : E_AppAbs; eauto.
+  have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity.
-  eauto using T_Conv.
+  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 n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+Lemma E_Pair Γ a0 b0 a1 b1 A B i :
-    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+  Γ ⊢ 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 => n a b Γ A.
+  move => hSig ha hb.
-  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity.
-  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\
-  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+                     Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity.
-  move /Su_Sig_Proj1 in hS.
+  have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt.
-  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac].
-  apply : E_Conv; eauto.
+  apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl.
-  apply : E_ProjPair1; eauto.
+  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 n Γ (a : PTm n) A :
+Lemma Suc_Inv Γ (a : PTm) A :
  Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
 Proof.
  move E : (PSuc a) => u hu.
  move : a E.
-  elim : n Γ u A /hu => //=.
+  elim : Γ u A /hu => //=.
-  - move => n Γ a ha iha a0 [*]. subst.
+  - move => Γ a ha iha a0 [*]. subst.
    split => //=. eapply wff_mutual in ha.
    apply : Su_Eq.
    apply E_Refl. by apply T_Nat'.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.
-Lemma RRed_Eq n Γ (a b : PTm n) A :
+Lemma RRed_Eq Γ (a b : PTm) A :
  Γ ⊢ a ∈ A ->
  RRed.R a b ->
  Γ ⊢ a ≡ b ∈ A.
 Proof.
-  move => + h. move : Γ A. elim : n a b /h => n.
+  move => + h. move : Γ A. elim : a b /h.
  - apply E_AppAbs.
  - move => p a b Γ A.
    case : p => //=.
@ -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.
@ -214,7 +165,7 @@ Proof.
  - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
 Qed.
-Theorem subject_reduction n Γ (a b A : PTm n) :
+Theorem subject_reduction Γ (a b A : PTm) :
  Γ ⊢ a ∈ A ->
  RRed.R a b ->
  Γ ⊢ b ∈ A.
--- a/theories/soundness.v
+++ b/theories/soundness.v
@ -1,15 +1,15 @@
-Require Import Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.unscoped Autosubst2.syntax.
 Require Import fp_red logrel typing.
 From Hammer Require Import Tactics.
 Theorem fundamental_theorem :
-  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
+  (forall Γ, ⊢ Γ -> ⊨ Γ) /\
-  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
+  (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
-  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
+  (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
-  (forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
+  (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.
-Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Lemma synsub_to_usub : forall Γ (a b : PTm), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
 Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.
--- a/theories/structural.v
+++ b/theories/structural.v
--- a/theories/termination.v
+++ b/theories/termination.v
@ -0,0 +1,5 @@
 Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable.
 From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 From stdpp Require Import relations (nsteps (..), rtc(..)).
 Import Psatz.
--- a/theories/typing.v
+++ b/theories/typing.v
@ -1,240 +1,230 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
 Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
 Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
 Reserved Notation "⊢ Γ" (at level 70).
-Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
-| T_Var n Γ (i : fin n) :
+| T_Var i Γ A :
  ⊢ Γ ->
-  Γ ⊢ VarPTm i ∈ Γ i
+  lookup i Γ A ->
  Γ ⊢ VarPTm i ∈ A
-| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
+| T_Bind Γ i p (A : PTm) (B : PTm) :
  Γ ⊢ A ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ PUniv i ->
  Γ ⊢ PBind p A B ∈ PUniv i
-| T_Abs n Γ (a : PTm (S n)) A B i :
+| T_Abs Γ (a : PTm) A B i :
  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
  Γ ⊢ PAbs a ∈ PBind PPi A B
-| T_App n Γ (b a : PTm n) A B :
+| T_App Γ (b a : PTm) A B :
  Γ ⊢ b ∈ PBind PPi A B ->
  Γ ⊢ a ∈ A ->
  Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B
-| T_Pair n Γ (a b : PTm n) A B i :
+| T_Pair Γ (a b : PTm) A B i :
  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊢ a ∈ A ->
  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
  Γ ⊢ PPair a b ∈ PBind PSig A B
-| T_Proj1 n Γ (a : PTm n) A B :
+| T_Proj1 Γ (a : PTm) A B :
  Γ ⊢ a ∈ PBind PSig A B ->
  Γ ⊢ PProj PL a ∈ A
-| T_Proj2 n Γ (a : PTm n) A B :
+| T_Proj2 Γ (a : PTm) A B :
  Γ ⊢ a ∈ PBind PSig A B ->
  Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
-| T_Univ n Γ i :
+| T_Univ Γ i :
  ⊢ Γ ->
-  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
+  Γ ⊢ PUniv i ∈ PUniv (S i)
-| T_Nat n Γ i :
+| T_Nat Γ i :
  ⊢ Γ ->
-  Γ ⊢ PNat : PTm n ∈ PUniv i
+  Γ ⊢ PNat ∈ PUniv i
-| T_Zero n Γ :
+| T_Zero Γ :
  ⊢ Γ ->
-  Γ ⊢ PZero : PTm n ∈ PNat
+  Γ ⊢ PZero ∈ PNat
-| T_Suc n Γ (a : PTm n) :
+| T_Suc Γ (a : PTm) :
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ PSuc a ∈ PNat
-| T_Ind s Γ P (a : PTm s) b c i :
+| T_Ind Γ P (a : PTm) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  cons PNat Γ ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P
-| T_Conv n Γ (a : PTm n) A B :
+| T_Conv Γ (a : PTm) A B :
  Γ ⊢ a ∈ A ->
  Γ ⊢ A ≲ B ->
  Γ ⊢ a ∈ B
-with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
+with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| E_Refl n Γ (a : PTm n) A :
+| E_Refl Γ (a : PTm ) A :
  Γ ⊢ a ∈ A ->
  Γ ⊢ a ≡ a ∈ A
-| E_Symmetric n Γ (a b : PTm n) A :
+| E_Symmetric Γ (a b : PTm) A :
  Γ ⊢ a ≡ b ∈ A ->
  Γ ⊢ b ≡ a ∈ A
-| E_Transitive n Γ (a b c : PTm n) A :
+| E_Transitive Γ (a b c : PTm) A :
  Γ ⊢ a ≡ b ∈ A ->
  Γ ⊢ b ≡ c ∈ A ->
  Γ ⊢ a ≡ c ∈ A
 (* Congruence *)
-| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
  ⊢ Γ ->
  Γ ⊢ A0 ∈ PUniv i ->
  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
-| E_Abs n Γ (a b : PTm (S n)) A B i :
+| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B ->
  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
 | E_App n Γ i (b0 b1 a0 a1 : PTm n) 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 n Γ (a0 a1 b0 b1 : PTm n) A B i :
+| E_Proj1 Γ (a b : PTm) A B :
  Γ ⊢ 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 n Γ (a b : PTm n) A B :
  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
-| E_Proj2 n Γ i (a b : PTm n) A B :
+| E_Proj2 Γ i (a b : PTm) A B :
  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
-| E_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
+| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
  Γ ⊢ a0 ≡ a1 ∈ PNat ->
  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
-  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
+  (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
  Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
-| E_SucCong n Γ (a b : PTm n) :
+| E_SucCong Γ (a b : PTm) :
  Γ ⊢ a ≡ b ∈ PNat ->
  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
-| E_Conv n Γ (a b : PTm n) A B :
+| E_Conv Γ (a b : PTm) A B :
  Γ ⊢ a ≡ b ∈ A ->
  Γ ⊢ A ≲ B ->
  Γ ⊢ a ≡ b ∈ B
 (* Beta *)
-| E_AppAbs n Γ (a : PTm (S n)) b A B i:
+| E_AppAbs Γ (a : PTm) b A B i:
  Γ ⊢ PBind PPi A B ∈ PUniv i ->
  Γ ⊢ b ∈ A ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
  Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
-| E_ProjPair1 n Γ (a b : PTm n) A B i :
+| E_ProjPair1 Γ (a b : PTm) A B i :
  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊢ a ∈ A ->
  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
  Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A
-| E_ProjPair2 n Γ (a b : PTm n) A B i :
+| E_ProjPair2 Γ (a b : PTm) A B i :
  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊢ a ∈ A ->
  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
  Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
-| E_IndZero n Γ P i (b : PTm n) c :
+| E_IndZero Γ P i (b : PTm) c :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
-| E_IndSuc s Γ P (a : PTm s) b c i :
+| E_IndSuc Γ P (a : PTm) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (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_FunExt Γ (a b : PTm) A B i :
-| E_AppEta n Γ (b : PTm n) A B i :
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
-  ⊢ Γ ->
+  Γ ⊢ a ∈ PBind PPi A B ->
  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
  Γ ⊢ 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 n Γ (a : PTm n) A B i :
+| E_PairExt Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv 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 : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| Su_Transitive  n Γ (A B C : PTm n) :
+| Su_Transitive Γ (A B C : PTm) :
  Γ ⊢ A ≲ B ->
  Γ ⊢ B ≲ C ->
  Γ ⊢ A ≲ C
 (* Congruence *)
-| Su_Univ n Γ i j :
+| Su_Univ Γ i j :
  ⊢ Γ ->
  i <= j ->
-  Γ ⊢ PUniv i : PTm n ≲ PUniv j
+  Γ ⊢ PUniv i ≲ PUniv j
-| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i :
+| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
  ⊢ Γ ->
  Γ ⊢ A0 ∈ PUniv i ->
  Γ ⊢ A1 ≲ A0 ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1 ->
  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
-| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i :
+| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
  ⊢ Γ ->
  Γ ⊢ A1 ∈ PUniv i ->
  Γ ⊢ A0 ≲ A1 ->
-  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
+  (cons A1 Γ) ⊢ B0 ≲ B1 ->
  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
 (* Injecting from equalities *)
-| Su_Eq n Γ (A : PTm n) B i  :
+| Su_Eq Γ (A : PTm) B i  :
  Γ ⊢ A ≡ B ∈ PUniv i ->
  Γ ⊢ A ≲ B
 (* Projection axioms *)
-| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
  Γ ⊢ A1 ≲ A0
-| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
  Γ ⊢ A0 ≲ A1
-| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
+| Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 :
  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
  Γ ⊢ a0 ≡ a1 ∈ A1 ->
  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
-| Su_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
+| Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
  Γ ⊢ a0 ≡ a1 ∈ A0 ->
  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
-with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
+with Wff : list PTm -> Prop :=
 | Wff_Nil :
-  ⊢ null
+  ⊢ nil
-| Wff_Cons n Γ (A : PTm n) i :
+| Wff_Cons Γ (A : PTm) i :
  ⊢ Γ ->
  Γ ⊢ A ∈ PUniv i ->
  (* -------------------------------- *)
-  ⊢ funcomp (ren_PTm shift) (scons A Γ)
+  ⊢ (cons A Γ)
 where
 "Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
@ -245,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
Yiyun Liu	437c97455e	Finish the soundness and completeness proof of the subtyping algorithm	2025-03-06 20:42:08 -05:00
Yiyun Liu	fe52d78ec5	Start the soundness proof for check_sub	2025-03-06 19:20:54 -05:00
Yiyun Liu	6f154cc9c6	Add stub for check_sub	2025-03-06 16:20:32 -05:00
Yiyun Liu	96b3139726	Prove termination	2025-03-06 15:39:27 -05:00
Yiyun Liu	b29d567ef0	Add termination	2025-03-05 00:18:28 -05:00
Yiyun Liu	c4f01d7dfc	Update the correctness proof of the computable function	2025-03-04 23:48:42 -05:00
Yiyun Liu	c1ff0ae145	Add check_equal_conf case	2025-03-04 23:22:41 -05:00
Yiyun Liu	c05bd10016	Turn off auto equations generation because it produces poor lemmas	2025-03-04 22:43:30 -05:00
Yiyun Liu	68cc482479	Fix the correctness proof	2025-03-04 22:30:21 -05:00
Yiyun Liu	a23be7f9b5	Simplify the definition of algo_dom	2025-03-04 22:28:18 -05:00
Yiyun Liu	5087b8c6ce	Add new definition of eq_view	2025-03-04 22:20:12 -05:00
Yiyun Liu	dcd4465310	Finish the proof of completeness for the algorithm	2025-03-04 21:47:57 -05:00
Yiyun Liu	b9b6899764	Half way done with check_equal_complete	2025-03-04 00:39:59 -05:00
Yiyun Liu	0060d3fb86	Factor out the rewriting lemmas	2025-03-04 00:27:42 -05:00
Yiyun Liu	87f6dcd870	Prove the soundness of the computable equality	2025-03-03 23:46:41 -05:00
Yiyun Liu	36d1f95d65	Move HRed to the common .v file	2025-03-03 21:16:42 -05:00
Yiyun Liu	5ac3b21331	Refactor the correctness proof of coquand's algorithm	2025-03-03 21:09:03 -05:00
Yiyun Liu	3a17548a7d	Minor	2025-03-03 16:01:28 -05:00
Yiyun Liu	3e8ad2c5bc	Work on the refactoring proof	2025-03-03 15:50:08 -05:00
Yiyun Liu	fe418c2a78	Fix preservation and broken cases in logrel	2025-03-03 15:29:50 -05:00
Yiyun Liu	d68adf85f4	Finish refactoring substitution lemmas	2025-03-03 15:22:59 -05:00
Yiyun Liu	896d22ac9b	minor	2025-03-03 01:40:12 -05:00
Yiyun Liu	b3bd75ad42	Fix the typing rules	2025-03-03 01:38:22 -05:00
Yiyun Liu	47e21df801	Finish refactoring logical relations	2025-03-03 01:15:21 -05:00
Yiyun Liu	7f38544a1e	Finish refactoring fp_red	2025-03-02 22:41:15 -05:00
Yiyun Liu	551dd5c17c	Fix the fv proof	2025-03-02 20:19:11 -05:00
Yiyun Liu	226b196d15	Refactor half of fp_red	2025-03-02 17:35:51 -05:00
Yiyun Liu	657c1325c9	Add unscoped syntax	2025-03-02 16:40:39 -05:00