Prove PairEta

Reviewed-on: #1

Makefile

@@ -16,12 +16,12 @@ uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
 theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
-	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
+	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
 
 FORCE:

syntax.sig

@@ -16,4 +16,7 @@ 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
+PInd : (bind PTm in PTm) -> PTm -> PTm -> (bind PTm,PTm in PTm) -> PTm

theories/Autosubst2/fintype.v

@@ -1,419 +0,0 @@
-(** * Autosubst Header for Scoped Syntax
-    Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact.
-
-Version: December 11, 2019.
-*)
-Require Import core.
-Require Import Setoid Morphisms Relation_Definitions.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
-  match p with eq_refl => eq_refl end.
-
-Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
-  match q with eq_refl => match p with eq_refl => eq_refl end end.
-
-(** ** Primitives of the Sigma Calculus
-    We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type.
-*)
-
-Fixpoint fin (n : nat) : Type :=
-  match n with
-  | 0 => False
-  | S m => option (fin m)
-  end.
-
-(** Renamings and Injective Renamings
-     _Renamings_ are mappings between finite types.
-*)
-Definition ren (m n : nat) : Type := fin m -> fin n.
-
-Definition id {X} := @Datatypes.id X.
-
-Definition idren {k: nat} : ren k k := @Datatypes.id (fin k).
-
-(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *)
-Definition var_zero {n : nat} : fin (S n) := None.
-
-Definition null {T} (i : fin 0) : T := match i with end.
-
-Definition shift {n : nat} : ren n (S n) :=
-  Some.
-
-(** Extension of Finite Mappings
-    Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows:
-*)
-Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X :=
-  match m with
-  | None => x
-  | Some i => f i
-  end.
-
-#[ export ]
-Hint Opaque scons : rewrite.
-
-(** ** Type Class Instances for Notation *)
-
-(** *** Type classes for renamings. *)
-
-Class Ren1 (X1  : Type) (Y Z : Type) :=
-  ren1 : X1 -> Y -> Z.
-
-Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
-  ren2 : X1 -> X2 -> Y -> Z.
-
-Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
-  ren3 : X1 -> X2 -> X3 -> Y -> Z.
-
-Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
-  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
-
-Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
-  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
-
-Module RenNotations.
-  Notation "s ⟨ xi1 ⟩" := (ren1  xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
-
-  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
-
-  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
-
-  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
-End RenNotations.
-
-(** *** Type Classes for Substiution *)
-
-Class Subst1 (X1 : Type) (Y Z: Type) :=
-  subst1 : X1 -> Y -> Z.
-
-Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
-  subst2 : X1 -> X2 -> Y  -> Z.
-
-Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
-  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
-
-Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
-  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
-
-Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
-  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
-
-Module SubstNotations.
-  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
-
-  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
-End SubstNotations.
-
-(** ** Type Class for Variables *)
-Class Var X Y :=
-  ids : X -> Y.
-
-
-(** ** Proofs for substitution primitives *)
-
-(** Forward Function Composition
-    Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour.
-    That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *)
-
-Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
-
-Module CombineNotations.
-  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
-
-  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
-
-  #[ global ]
-  Open Scope fscope.
-  #[ global ]
-  Open Scope subst_scope.
-End CombineNotations.
-
-Import CombineNotations.
-
-
-(** Generic lifting operation for renamings *)
-Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) :=
-  var_zero .: xi >> shift.
-
-(** Generic proof that lifting of renamings composes. *)
-Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
-  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
-Proof.
-  intros [x|].
-  - cbn. unfold funcomp. now rewrite <- E.
-  - reflexivity.
-Qed.
-
-Arguments up_ren_ren {k l m} xi zeta rho E.
-
-Lemma fin_eta {X} (f g : fin 0 -> X) :
-  pointwise_relation _ eq f g.
-Proof. intros []. Qed.
-
-(** Eta laws *)
-Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) :
-  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
-Proof. intros x. destruct x; reflexivity. Qed.
-
-Lemma scons_eta_id' {n : nat} :
-  pointwise_relation (fin (S n)) eq (var_zero .: shift) id.
-Proof. intros x. destruct x; reflexivity. Qed.
-
-Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) :
-  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
-Proof. intros x. destruct x; reflexivity. Qed.
-
-(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *)
-(*   pointwise_relation _ eq (funcomp (scons s f) shift) f. *)
-(* Proof. *)
-(*   reflexivity. *)
-(* Qed. *)
-
-(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *)
-(*   (scons s f (shift x)) = f x. *)
-(* Proof. *)
-(*   reflexivity. *)
-(* Qed. *)
-
-(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
-#[export] Instance scons_morphism {X: Type} {n:nat} :
-  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n).
-Proof.
-  intros t t' -> sigma tau H.
-  intros [x|].
-  cbn. apply H.
-  reflexivity.
-Qed.
-
-#[export] Instance scons_morphism2 {X: Type} {n: nat} :
-  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n).
-Proof.
-  intros ? t -> sigma tau H ? x ->.
-  destruct x as [x|].
-  cbn. apply H.
-  reflexivity.
-Qed.
-
-(** ** Variadic Substitution Primitives *)
-
-Fixpoint shift_p (p : nat) {n} : ren n (p + n) :=
-  fun n => match p with
-        | 0 => n
-        | S p => Some (shift_p p n)
-        end.
-
-Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n)  -> X.
-Proof.
-  destruct m.
-  - intros n f g. exact g.
-  - intros n f g. cbn. apply scons.
-    + exact (f var_zero).
-    + apply scons_p.
-      * intros z. exact (f (Some z)).
-      * exact g.
-Defined.
-
-#[export] Hint Opaque scons_p : rewrite.
-
-#[export] Instance scons_p_morphism {X: Type} {m n:nat} :
-  Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n).
-Proof.
-  intros sigma sigma' Hsigma tau tau' Htau.
-  intros x.
-  induction m.
-  - cbn. apply Htau.
-  - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
-    destruct x as [x|].
-    + cbn. apply IHm.
-      intros ?. apply Hsigma.
-    + cbn. apply Hsigma.
-Qed.
-
-#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} :
-  Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n).
-Proof.
-  intros sigma sigma' Hsigma tau tau' Htau ? x ->.
-  induction m.
-  - cbn. apply Htau.
-  - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x.
-    destruct x as [x|].
-    + cbn. apply IHm.
-      intros ?. apply Hsigma.
-    + cbn. apply Hsigma.
-Qed.
-
-Definition zero_p {m : nat} {n} : fin m -> fin (m + n).
-Proof.
-  induction m.
-  - intros [].
-  - intros [x|].
-    + exact (shift_p 1 (IHm x)).
-    + exact var_zero.
-Defined.
-
-Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z:
-  (scons_p  f g) (zero_p  z) = f z.
-Proof.
- induction m.
-  - inversion z.
-  - destruct z.
-    + simpl. simpl. now rewrite IHm.
-    + reflexivity.
-Qed.
-
-Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) :
-  pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f.
-Proof.
-  intros z.
-  unfold funcomp.
-  induction m.
-  - inversion z.
-  - destruct z.
-    + simpl. now rewrite IHm.
-    + reflexivity.
-Qed.
-
-Lemma scons_p_tail' X  m n (f : fin m -> X) (g : fin n -> X) z :
-  scons_p  f g (shift_p m z) = g z.
-Proof. induction m; cbn; eauto. Qed.
-
-Lemma scons_p_tail_pointwise X  m n (f : fin m -> X) (g : fin n -> X) :
-  pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g.
-Proof. intros z. induction m; cbn; eauto. Qed.
-
-Lemma destruct_fin {m n} (x : fin (m + n)):
-  (exists x', x = zero_p  x') \/ exists x', x = shift_p m x'.
-Proof.
-  induction m; simpl in *.
-  - right. eauto.
-  - destruct x as [x|].
-    + destruct (IHm x) as [[x' ->] |[x' ->]].
-      * left. now exists (Some x').
-      * right. eauto.
-    + left. exists None. eauto.
-Qed.
-
-Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) :
-  pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)).
-Proof.
-  intros x.
-  destruct (destruct_fin x) as [[x' ->]|[x' ->]].
-  (* TODO better way to solve this? *)
-  - revert x'.
-    apply pointwise_forall.
-    change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h).
-    now setoid_rewrite scons_p_head_pointwise.
-  - revert x'.
-    apply pointwise_forall.
-    change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h).
-    change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)).
-    now rewrite !scons_p_tail_pointwise.
-Qed.
-
-
-Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z:
-  (forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z.
-Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed.
-
-(** Generic n-ary lifting operation. *)
-Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n)  :=
-   scons_p  (zero_p ) (xi >> shift_p _).
-
-Arguments upRen_p p {m n} xi.
-
-(** Generic proof for composition of n-ary lifting. *)
-Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) :
-  forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x.
-Proof.
-  intros x. destruct (destruct_fin x) as [[? ->]|[? ->]].
-  - unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'.
-  - unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'.
-    now rewrite <- E.
-Qed.
-
-
-Arguments zero_p m {n}.
-Arguments scons_p  {X} m {n} f g.
-
-Lemma scons_p_eta {X} {m n} {f : fin m -> X}
-      {g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}:
-  (forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z.
-Proof.
-  intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]].
-  - rewrite scons_p_head'. eauto.
-  - rewrite scons_p_tail'. eauto.
-Qed.
-
-Arguments scons_p_eta {X} {m n} {f g} h {z}.
-Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}.
-
-(** ** Notations for Scoped Syntax *)
-
-Module ScopedNotations.
-  Include RenNotations.
-  Include SubstNotations.
-  Include CombineNotations.
-
-(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
-
-  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
-
-  Notation "↑" := (shift) : subst_scope.
-
-  #[global]
-  Open Scope fscope.
-  #[global]
-  Open Scope subst_scope.
-End ScopedNotations.
-
-
-(** ** Tactics for Scoped Syntax *)
-
-Tactic Notation "auto_case" tactic(t) :=  (match goal with
-                                           | [|- forall (i : fin 0), _] => intros []; t
-                                           | [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t
-                                           | [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t
-                                           | [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t
-                                           | [|- forall (i : fin (S _)), _] =>  intros [?|]; t
-                                           end).
-
-#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances.
-
-(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
-Ltac fsimpl :=
-  repeat match goal with
-         | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
-         | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
-         | [|- context [id ?s]] => change (id s) with s
-         | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *)
-         (* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *)
-         | [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s
-         | [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m)
-           (* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *)
-         | [|- context[idren >> ?f]] => change (idren >> f) with f
-         | [|- context[?f >> idren]] => change (f >> idren) with f
-         | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
-         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce
-         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce
-         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
-         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
-         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
-         | [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce
-         | [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce
-         (* | _ => progress autorewrite with FunctorInstances *)
-         | [|- context[funcomp (scons_p _ _ _) (zero_p _)]] =>
-           first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ]
-         | [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head'
-         | [|- context[funcomp (scons_p _ _ _) (shift_p _)]] =>
-           first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ]
-         | [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail'
-         | _ => first [progress minimize | progress cbn [shift scons scons_p] ]
-         end.

theories/Autosubst2/unscoped.v

@@ -0,0 +1,213 @@
+(** * Autosubst Header for Unnamed Syntax
+
+Version: December 11, 2019.
+ *)
+
+(* Adrian:
+ I changed this library a bit to work better with my generated code.
+ 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
+ 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
+Require Import core.
+Require Import Setoid Morphisms Relation_Definitions.
+
+Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
+  match p with eq_refl => eq_refl end.
+
+Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
+  match q with eq_refl => match p with eq_refl => eq_refl end end.
+
+(** ** Primitives of the Sigma Calculus. *)
+
+Definition shift  := S.
+
+Definition var_zero := 0.
+
+Definition id {X} := @Datatypes.id X.
+
+Definition scons {X: Type} (x : X) (xi : nat -> X) :=
+  fun n => match n with
+        | 0 => x
+        | S n => xi n
+        end.
+
+#[ export ]
+Hint Opaque scons : rewrite.
+
+(** ** Type Class Instances for Notation
+Required to make notation work. *)
+
+(** *** Type classes for renamings. *)
+
+Class Ren1 (X1  : Type) (Y Z : Type) :=
+  ren1 : X1 -> Y -> Z.
+
+Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
+  ren2 : X1 -> X2 -> Y -> Z.
+
+Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
+  ren3 : X1 -> X2 -> X3 -> Y -> Z.
+
+Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
+  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
+
+Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
+  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
+
+Module RenNotations.
+  Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
+
+  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
+
+  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
+End RenNotations.
+
+(** *** Type Classes for Substiution *)
+
+Class Subst1 (X1 : Type) (Y Z: Type) :=
+  subst1 : X1 -> Y -> Z.
+
+Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
+  subst2 : X1 -> X2 -> Y  -> Z.
+
+Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
+  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
+
+Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
+  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
+
+Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
+  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
+
+Module SubstNotations.
+  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
+
+  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
+End SubstNotations.
+
+(** *** Type Class for Variables *)
+
+Class Var X Y :=
+  ids : X -> Y.
+
+#[export] Instance idsRen : Var nat nat := id.
+
+(** ** Proofs for the substitution primitives. *)
+
+Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
+
+Module CombineNotations.
+  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
+
+  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
+
+  #[ global ]
+  Open Scope fscope.
+  #[ global ]
+  Open Scope subst_scope.
+End CombineNotations.
+
+Import CombineNotations.
+
+
+(** A generic lifting of a renaming. *)
+Definition up_ren (xi : nat -> nat) :=
+  0 .: (xi >> S).
+
+(** A generic proof that lifting of renamings composes. *)
+Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) :
+  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
+Proof.
+  intros [|x].
+  - reflexivity.
+  - unfold up_ren. cbn. unfold funcomp. f_equal. apply E.
+Qed.
+
+(** Eta laws. *)
+Lemma scons_eta' {T} (f : nat -> T) :
+  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_eta_id' :
+  pointwise_relation _ eq (var_zero .: shift) id.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
+  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
+Proof. intros x. destruct x; reflexivity. Qed.
+
+(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
+#[export] Instance scons_morphism {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H.
+  intros [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+#[export] Instance scons_morphism2 {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H ? x ->.
+  destruct x as [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+(** ** Generic lifting of an allfv predicate *)
+Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p.
+
+(** ** Notations for unscoped syntax *)
+Module UnscopedNotations.
+  Include RenNotations.
+  Include SubstNotations.
+  Include CombineNotations.
+  
+  (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
+
+  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
+
+  Notation "↑" := (shift) : subst_scope.
+
+  #[global]
+  Open Scope fscope.
+  #[global]
+  Open Scope subst_scope.
+End UnscopedNotations.
+
+(** ** Tactics for unscoped syntax *)
+
+(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *)
+Tactic Notation "auto_case" tactic(t) :=  (match goal with
+                                           | [|- forall (i : nat), _] => intros []; t
+                                           end).
+
+
+(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
+Ltac fsimpl :=
+  repeat match goal with
+         | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
+         | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
+         | [|- context [id ?s]] => change (id s) with s
+         | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h))
+         | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v
+         | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v
+         | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n)
+         | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
+         | [|- context[var_zero]] =>  change var_zero with 0
+         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f)
+         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta'
+         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
+         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
+         (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
+         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
+         | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
+                        end.

theories/admissible.v

@@ -0,0 +1,264 @@
+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 Inversion wff_inv with (forall Γ, ⊢ Γ) Sort Prop.
+
+Lemma T_Abs Γ (a : PTm ) A B :
+  (cons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PAbs a ∈ PBind PPi A B.
+Proof.
+  move => ha.
+  have [i hB] : exists i, (cons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have hΓ : ⊢  (cons A Γ) by sfirstorder use:wff_mutual.
+  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 ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof.
+  move => h0 h1.
+  have : Γ ⊢ A0 ∈ PUniv i by hauto l:on use:regularity.
+  have : ⊢ Γ by sfirstorder use:wff_mutual.
+  move : E_Bind h0 h1; repeat move/[apply].
+  firstorder.
+Qed.
+
+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.
+Proof.
+  move => h.
+  have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto l:on use:regularity.
+  move : E_App h. by repeat move/[apply].
+Qed.
+
+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.
+  move => h.
+  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.

theories/common.v

@@ -0,0 +1,601 @@
+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).
+
+Lemma lookup_deter i Γ A B :
+  lookup i Γ A ->
+  lookup i Γ B ->
+  A = B.
+Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed.
+
+Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
+Proof.  move => ->. apply here. Qed.
+
+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.
+  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
+  | 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 (a b : PTm) (ξ : nat -> nat) :
+  ren_inj ξ ->
+  ren_PTm ξ a = ren_PTm ξ b ->
+  a = b.
+Proof.
+  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 (a : PTm) :=
+  match a with
+  | PPair _ _ => true
+  | PAbs _ => true
+  | PUniv _ => true
+  | PBind _ _ _ => true
+  | PNat => true
+  | PSuc _ => true
+  | PZero => true
+  | _ => false
+  end.
+
+Definition toHF (a : PTm) :=
+  match a with
+  | PPair _ _ => H_Pair
+  | PAbs _ => H_Abs
+  | PUniv _ => H_Univ
+  | PBind p _ _ => H_Bind p
+  | PNat => H_Nat
+  | PSuc _ => H_Suc
+  | PZero => H_Zero
+  | _ => H_Bot
+  end.
+
+Fixpoint ishne (a : PTm) :=
+  match a with
+  | VarPTm _ => true
+  | PApp a _ => ishne a
+  | PProj _ a => ishne a
+  | PInd _ n _ _ => ishne n
+  | _ => false
+  end.
+
+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 _, _ => (~~ 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 (a : PTm)  (ξ : nat -> nat) :
+  isabs (ren_PTm ξ a) = isabs a.
+Proof. case : a => //=. Qed.
+
+Definition ispair_ren (a : PTm)  (ξ : nat -> nat) :
+  ispair (ren_PTm ξ a) = ispair a.
+Proof. case : a => //=. Qed.
+
+Definition ishne_ren (a : PTm)  (ξ : nat -> nat) :
+  ishne (ren_PTm ξ a) = ishne a.
+Proof. move : ξ. elim : a => //=. Qed.
+
+Lemma renaming_shift Γ A :
+  renaming_ok (cons A Γ) Γ shift.
+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.

theories/executable.v

@@ -0,0 +1,350 @@
+From Equations Require Import Equations.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
+Require Import Logic.PropExtensionality (propositional_extensionality).
+Require Import ssreflect ssrbool.
+Import Logic (inspect).
+From Ltac2 Require Import Ltac2.
+Import Ltac2.Constr.
+Set Default Proof Mode "Classic".
+
+
+Require Import ssreflect ssrbool.
+From Hammer Require Import Tactics.
+
+Ltac2 destruct_algo () :=
+  lazy_match! goal with
+  | [h : algo_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_equal_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [h : algo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
+  | _ => idtac
+  end.
+
+Ltac solve_check_equal :=
+  try solve [intros *;
+  match goal with
+  | [|- _ = _] => sauto
+  | _ => idtac
+  end].
+
+Global Set Transparent Obligations.
+
+Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
+
+Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
+  match a, b with
+  | VarPTm i, VarPTm j => nat_eqdec i j
+  | PAbs a, PAbs b => check_equal_r a b _
+  | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PPair a0 b0, PPair a1 b1 =>
+      check_equal_r a0 a1 _ && check_equal_r b0 b1 _
+  | PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PNat, PNat => true
+  | PZero, PZero => true
+  | PSuc a, PSuc b => check_equal_r a b _
+  | PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _
+  | PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _
+  | PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 =>
+      check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _
+  | PUniv i, PUniv j => nat_eqdec i j
+  | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _
+  | _, _ => false
+  end
+with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool :=
+  match fancy_hred a with
+  | inr a' => check_equal_r (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_equal_r a (proj1_sig b') _
+            | inl hb' => check_equal a b _
+            end
+  end.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
+  inversion h; subst => //=.
+  exfalso. sfirstorder use:algo_dom_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
+  exfalso. sfirstorder.
+Defined.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
+  destruct b' as [b' hb']. simpl.
+  inversion h; subst.
+  - exfalso.
+    sfirstorder use:algo_dom_no_hred.
+  - exfalso.
+    sfirstorder.
+  - assert (b' = b'0) by eauto using hred_deter. by subst.
+Defined.
+
+(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
+Next Obligation.
+  move => /= a b hdom ha _ hb _.
+  inversion hdom; subst.
+  - assumption.
+  - exfalso; sfirstorder.
+  - exfalso; sfirstorder.
+Defined.
+
+Lemma check_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h.
+Proof. reflexivity. Qed.
+
+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.
+  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.
+
+(* 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.

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.

theories/preservation.v

@@ -0,0 +1,172 @@
+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 Ind_Inv Γ P (a : PTm) b c U :
+  Γ ⊢ PInd P a b c ∈ U ->
+  exists i, (cons PNat Γ) ⊢ P ∈ PUniv i /\
+       Γ ⊢ a ∈ PNat /\
+       Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 : Γ 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.
+    eauto using E_Refl, Su_Eq.
+  - 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.
+Proof.
+  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.
+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.
+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.
+Qed.
+
+Lemma Suc_Inv Γ (a : PTm) A :
+  Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
+Proof.
+  move E : (PSuc a) => u hu.
+  move : a E.
+  elim : Γ u A /hu => //=.
+  - 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 Γ (a b : PTm) A :
+  Γ ⊢ a ∈ A ->
+  RRed.R a b ->
+  Γ ⊢ a ≡ b ∈ A.
+Proof.
+  move => + h. move : Γ A. elim : a b /h.
+  - apply E_AppAbs.
+  - move => p a b Γ A.
+    case : p => //=.
+    + apply E_ProjPair1.
+    + move /Proj2_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.
+      have : Γ ⊢ PPair a b ∈ PBind PSig A1 B1 by hauto lq:on ctrs:Wt.
+      move /T_Proj1.
+      move /E_ProjPair1 /E_Symmetric => h.
+      have /Su_Sig_Proj1 hSA := hS.
+      have : Γ ⊢ subst_PTm (scons a VarPTm) B1 ≲ subst_PTm (scons (PProj PL (PPair a b)) VarPTm) B0 by
+        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.
+  - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
+  - move => P a b c Γ A.
+    move /Ind_Inv.
+    move => [i][hP][ha][hb][hc]hSu.
+    apply : E_Conv; eauto.
+    apply : E_IndSuc'; eauto.
+    hauto l:on use:Suc_Inv.
+  - qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
+  - move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
+    have {}/iha iha := ih0.
+    have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+    apply : E_Conv; eauto.
+    apply : E_App; eauto using E_Refl.
+  - move => a0 b0 b1 ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
+    have {}/iha iha := ih1.
+    have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+    apply : E_Conv; eauto.
+    apply : E_App; eauto.
+    sfirstorder use:E_Refl.
+  - move => a0 a1 b ha iha Γ A /Pair_Inv.
+    move => [A0][B0][h0][h1]hU.
+    have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
+    have {}/iha iha := h0.
+    apply : E_Conv; eauto.
+    apply : E_Pair; eauto using E_Refl.
+  - move => a b0 b1 ha iha Γ A /Pair_Inv.
+    move => [A0][B0][h0][h1]hU.
+    have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
+    have {}/iha iha := h1.
+    apply : E_Conv; eauto.
+    apply : E_Pair; eauto using E_Refl.
+  - case.
+    + move => a0 a1 ha iha Γ A /Proj1_Inv [A0][B0][h0]hU.
+      apply : E_Conv; eauto.
+      qauto l:on ctrs:Eq,Wt.
+    + move => a0 a1 ha iha Γ A /Proj2_Inv [A0][B0][h0]hU.
+      have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+      apply : E_Conv; eauto.
+      apply : E_Proj2; eauto.
+  - move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
+    have {}/ihA ihA := h0.
+    apply : E_Conv; eauto.
+    apply E_Bind'; eauto using E_Refl.
+  - move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
+    have {}/ihA ihA := h1.
+    apply : E_Conv; eauto.
+    apply E_Bind'; eauto using E_Refl.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
+  - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
+Qed.
+
+Theorem subject_reduction Γ (a b A : PTm) :
+  Γ ⊢ a ∈ A ->
+  RRed.R a b ->
+  Γ ⊢ b ∈ A.
+Proof. hauto lq:on use:RRed_Eq, regularity. Qed.

theories/soundness.v

@@ -0,0 +1,15 @@
+Require Import Autosubst2.unscoped Autosubst2.syntax.
+Require Import fp_red logrel typing.
+From Hammer Require Import Tactics.
+
+Theorem fundamental_theorem :
+  (forall Γ, ⊢ Γ -> ⊨ Γ) /\
+  (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.
+  Unshelve. all : exact 0.
+Qed.
+
+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.

theories/structural.v

@@ -0,0 +1,845 @@
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing.
+From Hammer Require Import Tactics.
+Require Import ssreflect.
+Require Import Psatz.
+
+Lemma wff_mutual :
+  (forall Γ, ⊢ Γ -> True) /\
+  (forall Γ (a A : PTm), Γ ⊢ a ∈ A -> ⊢ Γ)  /\
+  (forall Γ (a b A : PTm), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\
+  (forall Γ (A B : PTm), Γ ⊢ A ≲ B -> ⊢ Γ).
+Proof. apply wt_mutual; eauto. Qed.
+
+#[export]Hint Constructors Wt Wff Eq : wt.
+
+Lemma T_Nat' Γ :
+  ⊢ Γ ->
+  Γ ⊢ PNat ∈ PUniv 0.
+Proof. apply T_Nat. Qed.
+
+Lemma renaming_up (ξ : nat -> nat) Δ Γ A :
+  renaming_ok Δ Γ ξ ->
+  renaming_ok (cons (ren_PTm ξ A) Δ) (cons A Γ) (upRen_PTm_PTm ξ) .
+Proof.
+  move => h i A0.
+  elim /lookup_inv => //=_.
+  - move => A1 Γ0 ? [*]. subst. apply here'. by asimpl.
+  - move => i0 Γ0 A1 B h' ? [*]. subst.
+    apply : there'; eauto. by asimpl.
+Qed.
+
+Lemma Su_Wt Γ a i :
+  Γ ⊢ a ∈ PUniv i ->
+  Γ ⊢ a ≲ a.
+Proof. hauto lq:on ctrs:LEq, Eq. Qed.
+
+Lemma Wt_Univ Γ a A i
+  (h : Γ ⊢ a ∈ A) :
+  Γ ⊢ @PUniv i ∈ PUniv (S i).
+Proof.
+  hauto lq:on ctrs:Wt use:wff_mutual.
+Qed.
+
+Lemma Bind_Inv Γ p (A : PTm) B U :
+  Γ ⊢ PBind p A B ∈ U ->
+  exists i, Γ ⊢ A ∈ PUniv i /\
+  (cons A Γ) ⊢ B ∈ PUniv i /\
+  Γ ⊢ PUniv i ≲ U.
+Proof.
+  move E :(PBind p A B) => T h.
+  move : p A B E.
+  elim : Γ T U / h => //=.
+  - move => Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst.
+    exists i. repeat split => //=.
+    eapply wff_mutual in hA.
+    apply Su_Univ; eauto.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma T_App' Γ (b a : PTm) A B U :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ PApp b a ∈ U.
+Proof. move => ->. apply T_App. Qed.
+
+Lemma T_Pair' Γ (a b : PTm ) A B i U :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ b ∈ U ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ PPair a b ∈ PBind PSig A B.
+Proof.
+  move => ->. eauto using T_Pair.
+Qed.
+
+Lemma E_IndCong' Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i U :
+  U = subst_PTm (scons a0 VarPTm) P0 ->
+  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
+  Γ ⊢ a0 ≡ a1 ∈ PNat ->
+  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) 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 ∈ U.
+Proof. move => ->. apply E_IndCong. Qed.
+
+Lemma T_Ind' Γ P (a : PTm) b c i U :
+  U = subst_PTm (scons a VarPTm) P ->
+  cons PNat Γ ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 ∈ U.
+Proof. move =>->. apply T_Ind. Qed.
+
+Lemma T_Proj2' Γ (a : PTm) A B U :
+  U = subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ∈ U.
+Proof. move => ->. apply T_Proj2. Qed.
+
+Lemma E_Proj2' Γ i (a b : PTm) A B U :
+  U = subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ U.
+Proof. move => ->. apply E_Proj2. Qed.
+
+Lemma E_Bind' Γ i p (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  cons A0 Γ ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof. hauto lq:on use:E_Bind, wff_mutual. Qed.
+
+Lemma E_App' Γ i (b0 b1 a0 a1 : PTm) A B U :
+  U = subst_PTm (scons a0 VarPTm) B ->
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ U.
+Proof. move => ->. apply E_App. Qed.
+
+Lemma E_AppAbs' Γ (a : PTm) b A B i u U :
+  u = subst_PTm (scons b VarPTm) a ->
+  U = subst_PTm (scons b VarPTm ) B ->
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ b ∈ A ->
+  cons A Γ ⊢ a ∈ B ->
+  Γ ⊢ PApp (PAbs a) b ≡ u ∈ U.
+  move => -> ->. apply E_AppAbs. Qed.
+
+Lemma E_ProjPair2' Γ (a b : PTm) A B i U :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ 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 Su_Pi_Proj2' Γ (a0 a1 A0 A1 : PTm ) B0 B1 U T :
+  U = subst_PTm (scons a0 VarPTm) B0 ->
+  T = subst_PTm (scons a1 VarPTm) B1 ->
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊢ a0 ≡ a1 ∈ A1 ->
+  Γ ⊢ U ≲ T.
+Proof. move => -> ->. apply Su_Pi_Proj2. Qed.
+
+Lemma Su_Sig_Proj2' Γ (a0 a1 A0 A1 : PTm) B0 B1 U T :
+  U = subst_PTm (scons a0 VarPTm) B0 ->
+  T = subst_PTm (scons a1 VarPTm) B1 ->
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊢ a0 ≡ a1 ∈ A0 ->
+  Γ ⊢ U ≲ T.
+Proof. move => -> ->. apply Su_Sig_Proj2. Qed.
+
+Lemma E_IndZero' Γ P i (b : PTm) c U :
+  U = subst_PTm (scons PZero VarPTm) P ->
+  cons PNat Γ ⊢ P ∈ PUniv i ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 ∈ U.
+Proof. move => ->. apply E_IndZero. Qed.
+
+Lemma Wff_Cons' Γ (A : PTm) i :
+  Γ ⊢ A ∈ PUniv i ->
+  (* -------------------------------- *)
+  ⊢ cons A Γ.
+Proof. hauto lq:on rew:off use:Wff_Cons, wff_mutual. Qed.
+
+Lemma E_IndSuc' Γ P (a : PTm) b c i u U :
+  u = subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c ->
+  U = subst_PTm (scons (PSuc a) VarPTm) P ->
+  cons PNat Γ ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 ≡ u ∈ U.
+Proof. move => ->->. apply E_IndSuc. Qed.
+
+Lemma renaming :
+  (forall Γ, ⊢ Γ -> True) /\
+  (forall Γ (a A : PTm), Γ ⊢ a ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\
+  (forall Γ (a b A : PTm), Γ ⊢ a ≡ b ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A) /\
+  (forall Γ (A B : PTm), Γ ⊢ A ≲ B -> forall  Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+    Δ ⊢ ren_PTm ξ A ≲ ren_PTm ξ B).
+Proof.
+  apply wt_mutual => //=; eauto 3 with wt.
+  - hauto lq:on rew:off ctrs:Wt, Wff  use:renaming_up.
+  - move => Γ a A B i hP ihP ha iha Δ ξ hΔ hξ.
+    apply : T_Abs; eauto.
+    move : ihP(hΔ) (hξ); repeat move/[apply]. move/Bind_Inv.
+    hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up.
+  - move => *. apply : T_App'; eauto. by asimpl.
+  - move => Γ a A b B i hA ihA hB ihB hS ihS Δ ξ hξ hΔ.
+    eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
+  - move => Γ a A B ha iha Δ ξ hΔ hξ. apply : T_Proj2'; eauto. by asimpl.
+  - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
+    move => [:hP].
+    apply : T_Ind'; eauto. by asimpl.
+    abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'.
+    hauto l:on use:renaming_up.
+    set x := subst_PTm _ _. have -> : x = ren_PTm ξ (subst_PTm (scons PZero VarPTm) P) by subst x; asimpl.
+    by subst x; eauto.
+    set Ξ := cons _ _.
+    have  hΞ : ⊢ Ξ. subst Ξ.
+    apply : Wff_Cons'; eauto. apply hP.
+    move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
+    set Ξ' := (cons _ _) .
+    have : renaming_ok Ξ Ξ' (upRen_PTm_PTm (upRen_PTm_PTm ξ)).
+    by do 2 apply renaming_up.
+    move /[swap] /[apply].
+    by asimpl.
+  - hauto lq:on ctrs:Wt,LEq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
+  - move => *. apply : E_App'; eauto. 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].
+    apply E_IndCong' with (i := i); eauto with wt.
+    by asimpl.
+    apply ihP0.
+    abstract : hP'.
+    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
+    abstract : hren.
+    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
+    apply ihP; eauto with wt.
+    move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ.
+    subst Ξ. apply :Wff_Cons'; eauto.
+    move /(_ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
+    move /(_ ltac:(qauto l:on use:renaming_up)).
+    suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
+      (ren_PTm shift
+         (subst_PTm
+            (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift)) P0)) = ren_PTm shift
+      (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift))
+         (ren_PTm (upRen_PTm_PTm ξ) P0)) by scongruence.
+    by asimpl.
+  - qauto l:on ctrs:Eq, LEq.
+  - move => Γ a b A B i hP ihP hb ihb ha iha Δ ξ hΔ hξ.
+    move : ihP (hξ) (hΔ). repeat move/[apply].
+    move /Bind_Inv.
+    move => [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    apply : E_AppAbs'; eauto. by asimpl. by asimpl.
+    hauto lq:on ctrs:Wff use:renaming_up.
+  - move => Γ a b A B i hP ihP ha iha hb ihb Δ ξ hΔ hξ.
+    move : {hP} ihP (hξ) (hΔ). repeat move/[apply].
+    move /Bind_Inv => [i0][h0][h1]h2.
+    have ? : Δ ⊢ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
+    apply : E_ProjPair1; eauto.
+    move : ihb hξ hΔ. repeat move/[apply]. by asimpl.
+  - move => Γ a b A B i hP ihP ha iha hb ihb Δ ξ hΔ hξ.
+    apply : E_ProjPair2'; eauto. by asimpl.
+    move : ihb hξ hΔ; repeat move/[apply]. by asimpl.
+  - move => Γ P i b c hP ihP hb ihb hc ihc Δ ξ hΔ hξ.
+    apply E_IndZero' with (i := i); eauto. by asimpl.
+    sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
+    move  /(_ Δ ξ hΔ) : ihb.
+    asimpl. by apply.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ by  sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
+    move /(_ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
+    set p := renaming_ok _ _ _.
+    have : p. by do 2 apply renaming_up.
+    move => /[swap]/[apply].
+    suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
+      (ren_PTm shift
+         (subst_PTm
+            (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift)) P))= ren_PTm shift
+      (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift))
+         (ren_PTm (upRen_PTm_PTm ξ) P)) by scongruence.
+    by asimpl.
+  - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
+    apply E_IndSuc' with (i := i). by asimpl. by asimpl.
+    sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
+    by eauto with wt.
+    move  /(_ Δ ξ hΔ) : ihb. asimpl. by apply.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ by  sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
+    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.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
+  - hauto lq:on ctrs:Wff use:Su_Sig, renaming_up.
+  - hauto q:on ctrs:LEq.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
+  - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
+Qed.
+
+Definition morphing_ok Δ Γ (ρ : nat -> PTm) :=
+  forall i A, lookup i Γ A -> Δ ⊢ ρ i ∈ subst_PTm ρ A.
+
+Lemma morphing_ren Ξ Δ Γ
+  (ρ : nat -> PTm) (ξ : nat -> nat) :
+  ⊢ Ξ ->
+  renaming_ok Ξ Δ ξ -> morphing_ok Δ Γ ρ ->
+  morphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
+Proof.
+  move => hΞ hξ hρ i A.
+  rewrite {1}/funcomp.
+  have -> :
+    subst_PTm (funcomp (ren_PTm ξ) ρ) A =
+    ren_PTm ξ (subst_PTm ρ A) by asimpl.
+  move => ?.  eapply renaming; eauto.
+Qed.
+
+Lemma morphing_ext Δ Γ (ρ : nat -> PTm) (a : PTm) (A : PTm)  :
+  morphing_ok Δ Γ ρ ->
+  Δ ⊢ a ∈ subst_PTm ρ A ->
+  morphing_ok
+    Δ (cons A Γ) (scons a ρ).
+Proof.
+  move => h ha i B.
+  elim /lookup_inv => //=_.
+  - move => A0 Γ0 ? [*]. subst.
+    by asimpl.
+  - move => i0 Γ0 A0 B0 h0 ? [*]. subst.
+    asimpl. by apply h.
+Qed.
+
+Lemma renaming_wt : forall Γ (a A : PTm), Γ ⊢ a ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ -> Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A.
+Proof. sfirstorder use:renaming. Qed.
+
+Lemma renaming_wt' : forall Δ Γ a A (ξ : nat -> nat) u U,
+    u = ren_PTm ξ a -> U = ren_PTm ξ A ->
+    Γ ⊢ a ∈ A -> ⊢ Δ ->
+    renaming_ok Δ Γ ξ -> Δ ⊢ u ∈ U.
+Proof. hauto use:renaming_wt. Qed.
+
+Lemma morphing_up Γ Δ (ρ : nat -> PTm) (A : PTm) k :
+  morphing_ok Γ Δ ρ ->
+  Γ ⊢ subst_PTm ρ A ∈ PUniv k ->
+  morphing_ok (cons (subst_PTm ρ A) Γ) (cons A Δ) (up_PTm_PTm ρ).
+Proof.
+  move => h h1 [:hp]. apply morphing_ext.
+  rewrite /morphing_ok.
+  move => i A0 hA0.
+  apply : renaming_wt'; last by apply renaming_shift.
+  rewrite /funcomp. reflexivity.
+  2 : { eauto. }
+  by asimpl.
+  abstract : hp. qauto l:on ctrs:Wff use:wff_mutual.
+  apply : T_Var;eauto. apply here'. by asimpl.
+Qed.
+
+Lemma weakening_wt : forall Γ (a A B : PTm) i,
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ a ∈ A ->
+    cons B Γ ⊢ ren_PTm shift a ∈ ren_PTm shift A.
+Proof.
+  move => Γ a A B i hB ha.
+  apply : renaming_wt'; eauto.
+  apply : Wff_Cons'; eauto.
+  apply : renaming_shift; eauto.
+Qed.
+
+Lemma weakening_wt' : forall Γ (a A B : PTm) i U u,
+    u = ren_PTm shift a ->
+    U = ren_PTm shift A ->
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ a ∈ A ->
+    cons B Γ ⊢ u ∈ U.
+Proof. move => > -> ->. apply weakening_wt. Qed.
+
+Lemma morphing :
+  (forall Γ, ⊢ Γ -> True) /\
+    (forall Γ a A, Γ ⊢ a ∈ A -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
+     Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A) /\
+    (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
+     Δ ⊢ subst_PTm ρ a ≡ subst_PTm ρ b ∈ subst_PTm ρ A) /\
+    (forall Γ A B, Γ ⊢ A ≲ B -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
+    Δ ⊢ subst_PTm ρ A ≲ subst_PTm ρ B).
+Proof.
+  apply wt_mutual => //=.
+  - hauto l:on unfold:morphing_ok.
+  - hauto lq:on use:morphing_up, Wff_Cons', T_Bind.
+  - move => Γ a A B i hP ihP ha iha Δ ρ hΔ hρ.
+    move : ihP (hΔ) (hρ); repeat move/[apply].
+    move /Bind_Inv => [j][h0][h1]h2. move {hP}.
+    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i by hauto lq:on ctrs:Wt.
+    apply : T_Abs; eauto.
+    apply : iha.
+    hauto lq:on use:Wff_Cons', Bind_Inv.
+    apply : morphing_up; eauto.
+  - move => *; apply : T_App'; eauto; by asimpl.
+  - move => Γ a A b B i hA ihA hB ihB hS ihS Δ ρ hρ hΔ.
+    eapply T_Pair' with (U := subst_PTm ρ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
+  - hauto lq:on use:T_Proj1.
+  - move => *. apply : T_Proj2'; eauto. by asimpl.
+  - hauto lq:on ctrs:Wt,LEq.
+  - qauto l:on ctrs:Wt.
+  - qauto l:on ctrs:Wt.
+  - qauto l:on ctrs:Wt.
+  - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
+    have  hξ' : morphing_ok (cons PNat Δ) (cons PNat Γ) (up_PTm_PTm ξ).
+    move /morphing_up : hξ.  move /(_ PNat 0).
+    apply. by apply T_Nat.
+    move => [:hP].
+    apply : T_Ind'; eauto. by asimpl.
+    abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'.
+    move /morphing_up : hξ.  move /(_ PNat 0).
+    apply. by apply T_Nat.
+    move : ihb hξ hΔ; do!move/[apply]. by asimpl.
+    set Ξ := cons _ _.
+    have  hΞ : ⊢ Ξ. subst Ξ.
+    apply : Wff_Cons'; eauto. apply hP.
+    move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
+    set Ξ' := (cons _ _) .
+    have : morphing_ok Ξ Ξ' (up_PTm_PTm (up_PTm_PTm ξ)).
+    eapply morphing_up; eauto. apply hP.
+    move /[swap]/[apply].
+    set x := (x in _ ⊢ _ ∈ x).
+    set y := (y in _ -> _ ⊢ _ ∈ y).
+    suff : x = y by scongruence.
+    subst x y. asimpl. substify. by asimpl.
+  - qauto l:on ctrs:Wt.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
+  - move => *. apply : E_App'; eauto. 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.
+    move => Δ ξ hΔ hξ.
+    have  hξ' : morphing_ok (cons PNat Δ)
+                   (cons PNat Γ) (up_PTm_PTm ξ).
+    move /morphing_up : hξ.  move /(_ PNat 0).
+    apply. by apply T_Nat.
+    move => [:hP'].
+    apply E_IndCong' with (i := i).
+    by asimpl.
+    abstract : hP'.
+    qauto l:on use:morphing_up, Wff_Cons', T_Nat'.
+    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
+    by eauto with wt.
+    move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ.
+    subst Ξ. apply :Wff_Cons'; eauto. apply hP'.
+    move /(_ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
+    move /(_ ltac:(qauto l:on use:morphing_up)).
+    asimpl. substify. by asimpl.
+  - eauto with wt.
+  - qauto l:on ctrs:Eq, LEq.
+  - move => Γ a b A B i hP ihP hb ihb ha iha Δ ρ hΔ hρ.
+    move : ihP (hρ) (hΔ). repeat move/[apply].
+    move /Bind_Inv.
+    move => [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    apply : E_AppAbs'; eauto. by asimpl. by asimpl.
+    hauto lq:on ctrs:Wff use:morphing_up.
+  - move => Γ a b A B i hP ihP ha iha hb ihb Δ ρ hΔ hρ.
+    move : {hP} ihP (hρ) (hΔ). repeat move/[apply].
+    move /Bind_Inv => [i0][h0][h1]h2.
+    have ? : Δ ⊢ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
+    apply : E_ProjPair1; eauto.
+    move : ihb hρ hΔ. repeat move/[apply]. by asimpl.
+  - move => Γ a b A B i hP ihP ha iha hb ihb Δ ρ hΔ hρ.
+    apply : E_ProjPair2'; eauto. by asimpl.
+    move : ihb hρ hΔ; repeat move/[apply]. by asimpl.
+  - move => Γ P i b c hP ihP hb ihb hc ihc Δ ξ hΔ hξ.
+    have  hξ' : morphing_ok (cons PNat Δ)(cons PNat Γ) (up_PTm_PTm ξ).
+    move /morphing_up : hξ.  move /(_ PNat 0).
+    apply. by apply T_Nat.
+    apply E_IndZero' with (i := i); eauto. by asimpl.
+    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
+    move  /(_ Δ ξ hΔ) : ihb.
+    asimpl. by apply.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
+    move /(_ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
+    move /(_ ltac:(sauto lq:on use:morphing_up)).
+    asimpl. substify. by asimpl.
+  - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
+    have  hξ' : morphing_ok (cons PNat Δ) (cons PNat Γ) (up_PTm_PTm ξ).
+    move /morphing_up : hξ.  move /(_ PNat 0).
+    apply. by apply T_Nat'.
+    apply E_IndSuc' with (i := i). by asimpl. by asimpl.
+    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
+    by eauto with wt.
+    move  /(_ Δ ξ hΔ) : ihb. asimpl. by apply.
+    set Ξ := cons _ _.
+    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
+    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.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
+  - hauto lq:on ctrs:Wff use:Su_Sig, morphing_up.
+  - hauto q:on ctrs:LEq.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
+  - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
+Qed.
+
+Lemma morphing_wt : forall Γ (a A : PTm ), Γ ⊢ a ∈ A -> forall Δ (ρ : nat -> PTm), ⊢ Δ -> morphing_ok Δ Γ ρ -> Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A.
+Proof. sfirstorder use:morphing. Qed.
+
+Lemma morphing_wt' : forall Δ Γ a A (ρ : nat -> PTm) u U,
+    u = subst_PTm ρ a -> U = subst_PTm ρ A ->
+    Γ ⊢ a ∈ A -> ⊢ Δ ->
+    morphing_ok Δ Γ ρ -> Δ ⊢ u ∈ U.
+Proof. hauto use:morphing_wt. Qed.
+
+Lemma morphing_id : forall Γ, ⊢ Γ -> morphing_ok Γ Γ VarPTm.
+Proof.
+  rewrite /morphing_ok => Γ hΓ i. asimpl.
+  eauto using T_Var.
+Qed.
+
+Lemma substing_wt : forall Γ (a : PTm) (b A : PTm) B,
+    (cons A Γ) ⊢ a ∈ B ->
+    Γ ⊢ b ∈ A ->
+    Γ ⊢ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm) B.
+Proof.
+  move => Γ a b A B ha hb [:hΓ]. apply : morphing_wt; eauto.
+  abstract : hΓ. sfirstorder use:wff_mutual.
+  apply morphing_ext; last by asimpl.
+  by apply morphing_id.
+Qed.
+
+(* Could generalize to all equal contexts *)
+Lemma ctx_eq_subst_one (A0 A1 : PTm) i j Γ a A :
+  (cons A0 Γ) ⊢ a ∈ A ->
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A1 ∈ PUniv j ->
+  Γ ⊢ A1 ≲ A0 ->
+  (cons A1 Γ) ⊢ a ∈ A.
+Proof.
+  move => h0 h1 h2 h3.
+  replace a with (subst_PTm VarPTm a); last by asimpl.
+  replace A with (subst_PTm VarPTm A); last by asimpl.
+  have ? : ⊢ Γ by sfirstorder use:wff_mutual.
+  apply : morphing_wt; eauto.
+  apply : Wff_Cons'; eauto.
+  move => k A2. elim/lookup_inv => //=_; cycle 1.
+  - move => i0 Γ0 A3 B hi ? [*]. subst.
+    asimpl.
+    eapply weakening_wt' with (a := VarPTm i0);eauto using T_Var.
+    by substify.
+  - move => A3 Γ0 ? [*]. subst.
+    move => [:hΓ'].
+    apply : T_Conv.
+    apply T_Var.
+    abstract : hΓ'.
+    eauto using Wff_Cons'. apply here.
+    asimpl. renamify.
+    eapply renaming; eauto.
+    apply : renaming_shift; eauto.
+Qed.
+
+Lemma bind_inst Γ p (A : PTm) B i a0 a1 :
+  Γ ⊢ PBind p A B ∈ PUniv i ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ subst_PTm (scons a0 VarPTm) B ≲ subst_PTm (scons a1 VarPTm) B.
+Proof.
+  move => h h0.
+  have {}h : Γ ⊢ PBind p A B ≲ PBind p A B by eauto using E_Refl, Su_Eq.
+  case : p h => //=; hauto l:on use:Su_Pi_Proj2, Su_Sig_Proj2.
+Qed.
+
+Lemma Cumulativity Γ (a : PTm ) i j :
+  i <= j ->
+  Γ ⊢ a ∈ PUniv i ->
+  Γ ⊢ a ∈ PUniv j.
+Proof.
+  move => h0 h1. apply : T_Conv; eauto.
+  apply Su_Univ => //=.
+  sfirstorder use:wff_mutual.
+Qed.
+
+Lemma T_Bind' Γ i j p (A : PTm ) (B : PTm) :
+  Γ ⊢ A ∈ PUniv i ->
+  (cons A Γ) ⊢ B ∈ PUniv j ->
+  Γ ⊢ PBind p A B ∈ PUniv (max i j).
+Proof.
+  move => h0 h1.
+  have [*] : i <= max i j /\ j <= max i j by lia.
+  qauto l:on ctrs:Wt use:Cumulativity.
+Qed.
+
+Hint Resolve T_Bind' : wt.
+
+Lemma regularity :
+  (forall Γ, ⊢ Γ -> forall i A, lookup i Γ A -> exists j, Γ ⊢ A ∈ PUniv j) /\
+    (forall Γ a A, Γ ⊢ a ∈ A -> exists i, Γ ⊢ A ∈ PUniv i)  /\
+    (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ A /\ exists i, Γ ⊢ A ∈ PUniv i) /\
+    (forall Γ A B, Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i /\ Γ ⊢ B ∈ PUniv i).
+Proof.
+  apply wt_mutual => //=; eauto with wt.
+  - move => i A. elim/lookup_inv => //=_.
+  - move => Γ A i hΓ ihΓ hA _ j A0.
+    elim /lookup_inv => //=_; cycle 1.
+    + move => i0 Γ0 A1 B + ? [*]. subst.
+      move : ihΓ => /[apply]. move => [j hA1].
+      exists j. apply : renaming_wt' => //=; eauto using renaming_shift. done.
+      apply : Wff_Cons'; eauto.
+    + move => A1 Γ0 ? [*]. subst.
+      exists i. apply : renaming_wt'; eauto. reflexivity.
+      econstructor; eauto.
+      apply : renaming_shift; eauto.
+  - move => Γ b a A B hb [i ihb] ha [j iha].
+    move /Bind_Inv : ihb => [k][h0][h1]h2.
+    move : substing_wt ha h1; repeat move/[apply].
+    move => h. exists k.
+    move : h. by asimpl.
+  - hauto lq:on use:Bind_Inv.
+  - move => Γ a A B ha [i /Bind_Inv[j][h0][h1]h2].
+    exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1.
+    move : substing_wt h1; repeat move/[apply].
+    by asimpl.
+  - move => Γ P a b c i + ? + *. clear. move => h ha. exists i.
+    hauto lq:on use:substing_wt.
+  - sfirstorder.
+  - sfirstorder.
+  - sfirstorder.
+  - move => Γ i p A0 A1 B0 B1 hΓ ihΓ hA0
+             [i0 ihA0] hA [ihA [ihA' [i1 ihA'']]].
+    repeat split => //=.
+    qauto use:T_Bind.
+    apply T_Bind; eauto.
+    sfirstorder.
+    apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
+    hauto lq:on.
+  - move => n i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]]
+             ha [iha0 [iha1 [i1 iha2]]].
+    repeat split.
+    qauto use:T_App.
+    apply : T_Conv; eauto.
+    qauto use:T_App.
+    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_Inv db:wt.
+  - move => Γ i a b A B hS _ hab [iha][ihb][j]ihs.
+    repeat split => //=; eauto with wt.
+    apply : T_Conv; eauto with wt.
+    move /E_Symmetric /E_Proj1 in hab.
+    eauto using bind_inst.
+    move /T_Proj1 in iha.
+    hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
+  - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i _ _ hPE [hP0 [hP1 _]] hae [ha0 [ha1 _]] _ [hb0 [hb1 hb2]] _ [hc0 [hc1 [j hc2]]].
+    have wfΓ : ⊢ Γ by hauto use:wff_mutual.
+    have wfΓ' : ⊢ (PNat :: Γ) by qauto use:Wff_Cons', T_Nat'.
+    repeat split. by eauto using T_Ind.
+    apply : T_Conv. apply : T_Ind; eauto.
+    apply : T_Conv; eauto.
+    eapply morphing; by eauto using Su_Eq, morphing_ext, morphing_id with wt.
+    apply : T_Conv.  apply : ctx_eq_subst_one; eauto.
+    by eauto using Su_Eq, E_Symmetric.
+    eapply renaming; eauto.
+    eapply morphing. apply : Su_Eq. apply hPE. apply wfΓ'.
+    apply morphing_ext.
+    replace (funcomp VarPTm shift) with (funcomp (@ren_PTm shift) VarPTm); last by asimpl.
+    apply : morphing_ren; eauto using morphing_id, renaming_shift.
+    apply T_Suc. apply T_Var=>//. apply here. apply : Wff_Cons'; eauto using T_Nat'.
+    apply renaming_shift.
+    have /E_Symmetric /Su_Eq : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv i by eauto with wt.
+    move /E_Symmetric in hae.
+    by eauto using Su_Sig_Proj2.
+    sauto lq:on use:substing_wt.
+  - hauto lq:on ctrs:Wt.
+  - hauto lq:on ctrs:Wt.
+  - hauto q:on use:substing_wt db:wt.
+  - hauto l:on use:bind_inst db:wt.
+  - move => Γ P i b c hP _ hb _ hc _.
+    have ? : ⊢ Γ by hauto use:wff_mutual.
+    repeat split=>//.
+    by eauto with wt.
+    sauto lq:on use:substing_wt.
+  - move => Γ P a b c i hP _ ha _ hb _ hc _.
+    have ? : ⊢ Γ by hauto use:wff_mutual.
+    repeat split=>//.
+    apply : T_Ind; eauto with wt.
+    set Ξ := (X in X ⊢ _ ∈ _) in hc.
+    have : morphing_ok Γ Ξ (scons (PInd P a b c) (scons a VarPTm)).
+    apply morphing_ext. apply morphing_ext. by apply morphing_id.
+    by eauto. by eauto with wt.
+    subst Ξ.
+    move : morphing_wt hc; repeat move/[apply]. asimpl. by apply.
+    sauto lq:on use:substing_wt.
+  - move => Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
+    have ? : ⊢ Γ by sfirstorder use:wff_mutual.
+    exists (max i j).
+    have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia.
+    qauto l:on use:T_Conv, Su_Univ.
+  - move => Γ i j hΓ *. exists (S (max i j)).
+    have [? ?] : S i <= S (Nat.max i j) /\ S j <= S (Nat.max i j) by lia.
+    hauto lq:on ctrs:Wt,LEq.
+  - move => Γ A0 A1 B0 B1 i hA0 _ hA1 [i0][ih0]ih1 hB[j0][ihB0]ihB1.
+    exists (max i0 j0).
+    split; eauto with wt.
+    apply T_Bind'; eauto.
+    sfirstorder use:ctx_eq_subst_one.
+  - move => n A0 A1 B0 B1 i hA1 _ hA0 [i0][ihA0]ihA1 hB[i1][ihB0]ihB1.
+    exists (max i0 i1). repeat split; eauto with wt.
+    apply T_Bind'; eauto.
+    sfirstorder use:ctx_eq_subst_one.
+  - sfirstorder.
+  - move => Γ A0 A1 B0 B1 _ [i][ih0 ih1].
+    move /Bind_Inv : ih0 => [i0][h _].
+    move /Bind_Inv : ih1 => [i1][h' _].
+    exists (max i0 i1).
+    have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
+    eauto using Cumulativity.
+  - move => Γ A0 A1 B0 B1 _ [i][ih0 ih1].
+    move /Bind_Inv : ih0 => [i0][h _].
+    move /Bind_Inv : ih1 => [i1][h' _].
+    exists (max i0 i1).
+    have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
+    eauto using Cumulativity.
+  - move => Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1.
+    move => [i][ihP0]ihP1.
+    move => ha [iha0][iha1][j]ihA1.
+    move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
+    move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
+    have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
+    exists (max i0 i1).
+    split.
+    + apply Cumulativity with (i := i0); eauto.
+      have : Γ ⊢ a0 ∈ A0 by eauto using T_Conv.
+      move : substing_wt ih0';repeat move/[apply]. by asimpl.
+    + apply Cumulativity with (i := i1); eauto.
+      move : substing_wt ih1' iha1;repeat move/[apply]. by asimpl.
+  - move => Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1.
+    move => [i][ihP0]ihP1.
+    move => ha [iha0][iha1][j]ihA1.
+    move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
+    move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
+    have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
+    exists (max i0 i1).
+    split.
+    + apply Cumulativity with (i := i0); eauto.
+      move : substing_wt iha0 ih0';repeat move/[apply]. by asimpl.
+    + apply Cumulativity with (i := i1); eauto.
+      have : Γ ⊢ a1 ∈ A1 by eauto using T_Conv.
+      move : substing_wt ih1';repeat move/[apply]. by asimpl.
+      Unshelve. all: exact 0.
+Qed.
+
+Lemma Var_Inv Γ (i : nat) A :
+  Γ ⊢ VarPTm i ∈ A ->
+  ⊢ Γ /\ exists B, lookup i Γ B /\ Γ ⊢ B ≲ A.
+Proof.
+  move E : (VarPTm i) => u hu.
+  move : i E.
+  elim : Γ u A / hu=>//=.
+  - move => i Γ A hΓ hi i0 [*]. subst.
+    split => //.
+    exists A. split => //.
+    have h : Γ ⊢ VarPTm i ∈ A by eauto using T_Var.
+    eapply regularity in h.
+    move : h => [i0]?.
+    apply : Su_Eq. apply E_Refl; eassumption.
+  - sfirstorder use:Su_Transitive.
+Qed.
+
+Lemma renaming_su' : forall Δ Γ ξ (A B : PTm) u U ,
+    u = ren_PTm ξ A ->
+    U = ren_PTm ξ B ->
+    Γ ⊢ A ≲ B ->
+    ⊢ Δ -> renaming_ok Δ Γ ξ ->
+    Δ ⊢ u ≲ U.
+Proof. move => > -> ->. hauto l:on use:renaming. Qed.
+
+Lemma weakening_su : forall Γ (A0 A1 B : PTm) i,
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ A0 ≲ A1 ->
+    (cons B Γ) ⊢ ren_PTm shift A0 ≲ ren_PTm shift A1.
+Proof.
+  move => Γ A0 A1 B i hB hlt.
+  apply : renaming_su'; eauto.
+  apply : Wff_Cons'; eauto.
+  apply : renaming_shift; eauto.
+Qed.
+
+Lemma regularity_sub0 : forall Γ (A B : PTm), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i.
+Proof. hauto lq:on use:regularity. Qed.
+
+Lemma Su_Pi_Proj2_Var Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  cons A1 Γ ⊢ B0 ≲ B1.
+Proof.
+  move => h.
+  have /Su_Pi_Proj1 h1 := h.
+  have /regularity_sub0 [i h2] := h1.
+  move /weakening_su : (h) h2. move => /[apply].
+  move => h2.
+  apply : Su_Pi_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
+  apply E_Refl. apply T_Var with (i := var_zero); eauto.
+  sfirstorder use:wff_mutual.
+  apply here.
+  by asimpl; rewrite subst_scons_id.
+  by asimpl; rewrite subst_scons_id.
+Qed.
+
+Lemma Su_Sig_Proj2_Var Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1.
+Proof.
+  move => h.
+  have /Su_Sig_Proj1 h1 := h.
+  have /regularity_sub0 [i h2] := h1.
+  move /weakening_su : (h) h2. move => /[apply].
+  move => h2.
+  apply : Su_Sig_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
+  apply E_Refl. apply T_Var with (i := var_zero); eauto.
+  sfirstorder use:wff_mutual.
+  apply here.
+  by asimpl; rewrite subst_scons_id.
+  by asimpl; rewrite subst_scons_id.
+Qed.

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.

theories/typing.v

@@ -0,0 +1,237 @@
+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 : list PTm -> PTm -> PTm -> Prop :=
+| T_Var i Γ A :
+  ⊢ Γ ->
+  lookup i Γ A ->
+  Γ ⊢ VarPTm i ∈ A
+
+| T_Bind Γ i p (A : PTm) (B : PTm) :
+  Γ ⊢ A ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ PUniv i ->
+  Γ ⊢ PBind p A B ∈ PUniv i
+
+| T_Abs Γ (a : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  (cons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PAbs a ∈ PBind PPi 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 Γ (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 Γ (a : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ∈ A
+
+| T_Proj2 Γ (a : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
+
+| T_Univ Γ i :
+  ⊢ Γ ->
+  Γ ⊢ PUniv i ∈ PUniv (S i)
+
+| T_Nat Γ i :
+  ⊢ Γ ->
+  Γ ⊢ PNat ∈ PUniv i
+
+| T_Zero Γ :
+  ⊢ Γ ->
+  Γ ⊢ PZero ∈ PNat
+
+| T_Suc Γ (a : PTm) :
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ PSuc a ∈ PNat
+
+| T_Ind Γ P (a : PTm) b c i :
+  cons PNat Γ ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 Γ (a : PTm) A B :
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ a ∈ B
+
+with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
+(* Structural *)
+| E_Refl Γ (a : PTm ) A :
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ a ≡ a ∈ A
+
+| E_Symmetric Γ (a b : PTm) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ a ∈ A
+
+| E_Transitive Γ (a b c : PTm) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ c ∈ A ->
+  Γ ⊢ a ≡ c ∈ A
+
+(* Congruence *)
+| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
+
+| 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_Proj1 Γ (a b : PTm) A B :
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
+
+| 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 Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
+  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
+  Γ ⊢ a0 ≡ a1 ∈ PNat ->
+  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) 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 Γ (a b : PTm) :
+  Γ ⊢ a ≡ b ∈ PNat ->
+  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
+
+| E_Conv Γ (a b : PTm) A B :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ a ≡ b ∈ B
+
+(* Beta *)
+| E_AppAbs Γ (a : PTm) b A B i:
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ b ∈ A ->
+  (cons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
+
+| 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 Γ (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 Γ P i (b : PTm) c :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 Γ P (a : PTm) b c i :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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
+
+| E_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
+
+| E_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
+
+with LEq : list PTm -> PTm -> PTm -> Prop :=
+(* Structural *)
+| Su_Transitive Γ (A B C : PTm) :
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ B ≲ C ->
+  Γ ⊢ A ≲ C
+
+(* Congruence *)
+| Su_Univ Γ i j :
+  ⊢ Γ ->
+  i <= j ->
+  Γ ⊢ PUniv i ≲ PUniv j
+
+| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A1 ≲ A0 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
+
+| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
+  Γ ⊢ A1 ∈ PUniv i ->
+  Γ ⊢ A0 ≲ A1 ->
+  (cons A1 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
+
+(* Injecting from equalities *)
+| Su_Eq Γ (A : PTm) B i  :
+  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B
+
+(* Projection axioms *)
+| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊢ A1 ≲ A0
+
+| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊢ A0 ≲ A1
+
+| 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 Γ (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 : list PTm -> Prop :=
+| Wff_Nil :
+  ⊢ nil
+| Wff_Cons Γ (A : PTm) i :
+  ⊢ Γ ->
+  Γ ⊢ A ∈ PUniv i ->
+  (* -------------------------------- *)
+  ⊢ (cons A Γ)
+
+where
+"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
+
+Scheme wf_ind := Induction for Wff Sort Prop
+  with wt_ind := Induction for Wt Sort Prop
+  with eq_ind := Induction for Eq Sort Prop
+  with le_ind := Induction for LEq Sort Prop.
+
+Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.