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 ucoq -o theories/Autosubst2/syntax.v syntax.sig
+	autosubst -f -v ge813 -s coq -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/unscoped.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 
 FORCE:

syntax.sig

@@ -16,7 +16,4 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
-PNat : PTm
-PZero : PTm
-PSuc : PTm -> PTm
-PInd : (bind PTm in PTm) -> PTm -> PTm -> (bind PTm,PTm in PTm) -> PTm
+PBot : PTm

theories/Autosubst2/fintype.v

@@ -0,0 +1,419 @@
+(** * 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

@@ -1,213 +0,0 @@
-(** * 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

@@ -1,264 +0,0 @@
-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

@@ -1,601 +0,0 @@
-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

@@ -1,350 +0,0 @@
-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

@@ -1,259 +0,0 @@
-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

@@ -1,172 +0,0 @@
-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

@@ -1,15 +0,0 @@
-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

@@ -1,845 +0,0 @@
-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

@@ -1,5 +0,0 @@
-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

@@ -1,237 +0,0 @@
-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.