10 changed files with 270 additions and 409 deletions
--- a/.woodpecker.yaml
+++ b/.woodpecker.yaml
@ -1,13 +0,0 @@
-when:
-  - event: [push, pull_request]
-    branch: [master]
-
-steps:
-  - name: build
-    image: coqorg/coq:8.20.1-ocaml-4.14.2-flambda
-    commands:
-      - opam update
-      - opam install -y coq-hammer-tactics coq-equations coq-stdpp coq-autosubst-ocaml
-      - eval $(opam env)
-      - sudo chown -R 1000:1000 .
-      - make -j2
--- a/README.org
+++ b/README.org
@ -1,6 +1,4 @@
 * Church Rosser, surjective pairing, and strong normalization
-[[https://woodpecker.electriclam.com/api/badges/3/status.svg]]
-
 This repository contains a mechanized proof that the lambda calculus
 with beta and eta rules for functions and pairs is in fact confluent
 for the subset of terms that are "strongly $\beta$-normalizing".
--- a/theories/admissible.v
+++ b/theories/admissible.v
@ -16,70 +16,6 @@ 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 ->
@ -110,155 +46,3 @@ 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
@ -586,8 +586,7 @@ Proof.
    have [h2 h3] : Γ ⊢ A2 ≲ A0 /\ Γ ⊢ A2 ≲ A1 by hauto l:on use:Su_Pi_Proj1.
    apply E_Conv with (A := PBind PPi A2 B2); cycle 1.
    eauto using E_Symmetric, Su_Eq.
-    apply : E_Abs; eauto.
-
+    apply : E_Abs; eauto. hauto l:on use:regularity.
    apply iha.
    move /Su_Pi_Proj2_Var in hp0.
    apply : T_Conv; eauto.
@ -608,12 +607,13 @@ Proof.
    have /regularity_sub0 [i' hPi0] := hPi.
    have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi A2 B2.
    apply : E_AppEta; eauto.
+    hauto l:on use:regularity.
    apply T_Conv with (A := A);eauto.
    eauto using Su_Eq.
    move => ?.
    suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi A2 B2
      by eauto using E_Transitive.
-    apply : E_Abs; eauto.
+    apply : E_Abs; eauto. hauto l:on use:regularity.
    apply iha.
    move /Su_Pi_Proj2_Var in hPi'.
    apply : T_Conv; eauto.
@ -665,7 +665,7 @@ Proof.
    have hA02 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Sig_Proj1.
    have hu'  : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
    move => [:ih0'].
-    apply : E_Transitive; last (apply : E_PairEta).
+    apply : E_Transitive; last (apply E_Symmetric; apply : E_PairEta).
    apply : E_Pair; eauto. hauto l:on use:regularity.
    abstract : ih0'.
    apply ih0. apply : T_Conv; eauto.
@ -678,6 +678,7 @@ Proof.
    move /E_Symmetric in ih0'.
    move /regularity_sub0 in hA'.
    hauto l:on use:bind_inst.
+    hauto l:on use:regularity.
    eassumption.
  (* Same as before *)
  - move {hAppL}.
@ -1322,7 +1323,7 @@ Qed.

 Lemma ce_neu_neu_helper a b :
  ishne a -> ishne b ->
-  (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b).
+  (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
 Proof. sauto lq:on. Qed.

 Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
@ -1332,7 +1333,7 @@ Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
 Proof. hauto q:on use:REReds.hne_ind_inv. Qed.

 Lemma coqeq_complete' :
-  (forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b)) /\
+  (forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\
    (forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
  move => [:hConfNeuNf hhPairNeu hhAbsNeu].
  apply algo_dom_mutual.
@ -1452,18 +1453,17 @@ Lemma coqeq_complete' :
  - move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B.
    move /Var_Inv => [h [A0 [h0 h1]]].
    move /Var_Inv => [h' [A1 [h0' h1']]].
-    by constructor.
+    split. by constructor.
+    suff : A0 = A1 by hauto lq:on db:wt.
+    eauto using lookup_deter.
  - move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja].
    apply ce_neu_neu_helper => //= Γ A B.
    move /App_Inv => [A0][B0][hb0][ha0]hS0.
    move /App_Inv => [A1][B1][hb1][ha1]hS1.
    move /(_ hju) : ihu.
    move => [_ ihb].
-    move : ihb (neu0) (neu1) (hb0) (hb1). repeat move/[apply].
-    move => ihb.
-    have : exists C, Γ ⊢ C ≲ PBind PPi A0 B0 /\ Γ ⊢ C ≲ PBind PPi A1 B1
-        by hauto lq:on use:coqeq_sound_mutual.
-    move => [C][hT0]hT1.
+    move : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply].
+    move => [hb01][C][hT0][hT1][hT2]hT3.
    move /Sub_Bind_InvL : (hT0).
    move => [i][A2][B2]hE.
    have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
@ -1478,7 +1478,26 @@ Lemma coqeq_complete' :
    move => iha.
    move : iha (ha0') (ha1'); repeat move/[apply].
    move => iha.
-    hauto lq:on ctrs:CoqEq_Neu.
+    split. sauto lq:on.
+    exists (subst_PTm (scons a0 VarPTm) B2).
+    split.
+    apply : Su_Transitive; eauto.
+    move /E_Refl in ha0.
+    hauto l:on use:Su_Pi_Proj2.
+    have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual.
+    split.
+    apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2).
+    move /regularity_sub0 : hSu10 => [i0].
+    hauto l:on use:bind_inst.
+    hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl.
+    split.
+    by apply : T_App; eauto using T_Conv_E.
+    apply : T_Conv; eauto.
+    apply T_App with (A := A2) (B := B2); eauto.
+    apply : T_Conv_E; eauto.
+    move /E_Symmetric in h01.
+    move /regularity_sub0 : hSu20 => [i0].
+    sfirstorder use:bind_inst.
  - move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst.
    move : iha hja; repeat move/[apply].
    move => [_ iha]. apply ce_neu_neu_helper => // Γ A B.
@ -1488,24 +1507,50 @@ Lemma coqeq_complete' :
    ** move => ha0 ha1.
       move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
       move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
-       move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
-       move => ih hnea0 hnea1.
-       have [C [hS0 hS1]] : exists C, Γ ⊢ C ≲ PBind PSig A0 B0 /\ Γ ⊢ C ≲ PBind PSig A1 B1
-           by hauto lq:on use:coqeq_sound_mutual.
+       move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
       move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
       have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
         by eauto using Su_Transitive, Su_Eq.
       have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
         by eauto using Su_Transitive, Su_Eq.
-       hauto lq:on ctrs:CoqEq_Neu.
+       exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive.
+       repeat split => //=.
+       hauto l:on use:Su_Sig_Proj1, Su_Transitive.
+       apply T_Proj1 with (B := B2); eauto using T_Conv_E.
+       apply T_Proj1 with (B := B2); eauto using T_Conv_E.
    ** move => ha0  ha1.
       move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
       move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
-       move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply]. move => ih hnea0 hnea1.
-       have [C [hS0 hS1]] : exists C, Γ ⊢ C ≲ PBind PSig A0 B0 /\ Γ ⊢ C ≲ PBind PSig A1 B1
-           by hauto lq:on use:coqeq_sound_mutual.
+       move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
+       move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
+       split. sauto lq:on.
       move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
-       hauto lq:on ctrs:CoqEq_Neu.
+       have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
+         by eauto using Su_Transitive, Su_Eq.
+       have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
+         by eauto using Su_Transitive, Su_Eq.
+       have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1.
+       have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1.
+       have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+       have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
+       have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2
+         by sauto lq:on use:coqeq_sound_mutual.
+       exists (subst_PTm (scons (PProj PL a0) VarPTm) B2).
+       repeat split.
+       *** apply : Su_Transitive; eauto.
+           have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2
+             by qauto use:regularity, E_Refl.
+           sfirstorder use:Su_Sig_Proj2.
+       *** apply : Su_Transitive; eauto.
+           sfirstorder use:Su_Sig_Proj2.
+       *** eauto using T_Proj2.
+       *** apply : T_Conv.
+           apply : T_Proj2; eauto.
+           move /E_Symmetric in haE.
+           move /regularity_sub0 in hSu21.
+           sfirstorder use:bind_inst.
  - move {hhPairNeu hhAbsNeu}.
    move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP  domu ihu domb ihb domc ihc /hne_ind_inj.
    move => /(_ neu0 neu1)  [hjP][hju][hjb]hjc.
@ -1542,7 +1587,16 @@ Lemma coqeq_complete' :
    apply : morphing_ren; eauto using renaming_shift. by apply morphing_id.
    apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
    have {}ihc : c0 ⇔ c1 by qauto l:on.
-    hauto q:on ctrs:CoqEq_Neu.
+    move => [:ih].
+    split. abstract : ih. move : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on.
+    have hEInd : Γ ⊢ PInd P0 u0 b0 c0 ≡ PInd P1 u1 b1 c1 ∈ subst_PTm (scons u0 VarPTm) P0 by hfcrush use:coqeq_sound_mutual.
+    exists (subst_PTm (scons u0 VarPTm) P0).
+    repeat split => //=; eauto with wt.
+    apply : Su_Transitive.
+    apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
+    apply : Su_Eq. apply E_Refl. by apply T_Nat'.
+    apply : Su_Eq. apply hPE. by eauto.
+    move : hEInd. clear. hauto l:on use:regularity.
  - move => a b ha hb.
    move {hhPairNeu hhAbsNeu}.
    case : hb; case : ha.
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@ -719,8 +719,6 @@ Module RRed.
    move => */=; apply : IndSuc'; eauto. by asimpl.
  Qed.

-  Lemma abs_preservation a b : isabs a -> R a b -> isabs b. hauto q:on inv:R. Qed.
-
 End RRed.

 Module RPar.
@ -1006,9 +1004,6 @@ Qed.

 Module RReds.

-  Lemma abs_preservation a b : isabs a -> rtc RRed.R a b -> isabs b.
-    induction 2; hauto lq:on use:RRed.abs_preservation. Qed.
-
  #[local]Ltac solve_s_rec :=
  move => *; eapply rtc_l; eauto;
         hauto lq:on ctrs:RRed.R.
@ -1760,15 +1755,6 @@ Module ERed.

  Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.

-  Lemma abs_back_preservation (a b : PTm) :
-    SN a -> R a b -> isabs b -> isabs a.
-  Proof.
-    move => + h.
-    elim : a b /h => //=.
-    case => //=. move => p. move /SN_NoForbid.P_PairInv.
-    sfirstorder use:SN_NoForbid.PProj_imp.
-  Qed.
-
  Lemma ToEPar (a b : PTm) :
    ERed.R a b -> EPar.R a b.
  Proof.
@ -3306,6 +3292,7 @@ Module DJoin.
  Qed.
 End DJoin.

+
 Module Sub1.
  Inductive R : PTm -> PTm -> Prop :=
  | Refl a :
--- a/theories/logrel.v
+++ b/theories/logrel.v
@ -619,6 +619,10 @@ 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.
@ -759,34 +763,6 @@ 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.
@ -808,6 +784,25 @@ 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 ->
@ -824,7 +819,7 @@ Lemma ST_Var Γ (i : nat) A :
  ⊨ Γ ->
  lookup i Γ A ->
  Γ ⊨ VarPTm i ∈ A.
-Proof. hauto l:on use:ST_Var', SemWff_lookup. Qed.
+Proof. hauto l:on use:ST_Var' unfold:SemWff. Qed.

 Lemma InterpUniv_Bind_nopf p i (A : PTm) B PA :
  ⟦ A ⟧ i ↘ PA ->
@ -1521,36 +1516,6 @@ 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.
@ -1701,4 +1666,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 SE_PairExt SE_FunExt : 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 : sem.
--- a/theories/preservation.v
+++ b/theories/preservation.v
@ -1,9 +1,80 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red.
 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 ->
@ -22,58 +93,36 @@ Proof.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.

-Lemma E_Abs Γ a b A B :
-  A :: Γ ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
+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.
-  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.
+  apply : E_Conv; eauto.
+  apply : E_AppAbs; eauto.
+  eauto using T_Conv.
 Qed.

-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.
+Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
 Proof.
-  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.
+  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 Suc_Inv Γ (a : PTm) A :
@ -110,7 +159,7 @@ Proof.
        apply : Su_Sig_Proj2; eauto.
      move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
      move {hS}.
-      move => ?. apply : E_Conv; eauto. apply : typing.E_ProjPair2; eauto.
+      move => ?. apply : E_Conv; eauto. apply : 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.
+  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
  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,7 +222,17 @@ 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].
@ -292,12 +302,9 @@ Proof.
    move /(_ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(by eauto using renaming_up)).
    by asimpl.
-  - 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.
+  - move => *.
+    apply : E_AppEta'; eauto. by asimpl.
+  - qauto l:on use:E_PairEta.
  - hauto lq:on ctrs:LEq.
  - qauto l:on ctrs:LEq.
  - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
@ -440,7 +447,17 @@ 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.
@ -507,14 +524,9 @@ Proof.
    move /(_ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(sauto l:on use:morphing_up)).
    asimpl. substify. by asimpl.
-  - 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.
+  - move => *.
+    apply : E_AppEta'; eauto. by asimpl.
+  - qauto l:on use:E_PairEta.
  - hauto lq:on ctrs:LEq.
  - qauto l:on ctrs:LEq.
  - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
@ -655,6 +667,7 @@ 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.
@ -664,6 +677,7 @@ 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.
@ -712,6 +726,15 @@ 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/typing.v
+++ b/theories/typing.v
@ -89,12 +89,23 @@ 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
@ -153,20 +164,16 @@ 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

-| E_FunExt Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ PUniv i ->
-  Γ ⊢ a ∈ PBind PPi A B ->
+(* Eta *)
+| E_AppEta Γ (b : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
  Γ ⊢ 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
+  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B

-| E_PairExt Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ PUniv i ->
+| E_PairEta Γ (a : 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
+  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B

 with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
@ -235,3 +242,10 @@ 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. ... *)