Makefile

@@ -6,7 +6,7 @@ theories: $(COQMAKEFILE) FORCE
 validate: $(COQMAKEFILE) FORCE
 	$(MAKE) -f $(COQMAKEFILE) validate
 
-$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v
+$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 	$(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE)
 
 install: $(COQMAKEFILE)
@@ -15,13 +15,13 @@ install: $(COQMAKEFILE)
 uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
-theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v : syntax.sig
-	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
+theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
+	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
-	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v theories/Autosubst2/unscoped.v
+	rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
 
 FORCE:

syntax.sig

@@ -1,29 +1,16 @@
 nat  : Type
-PTm(VarPTm) : Type
 Tm(VarTm) : Type
 PTag : Type
 TTag : Type
-bool : Type
 
-PL : PTag
-PR : PTag
 TPi : TTag
 TSig : TTag
-
-PAbs : (bind PTm in PTm) -> PTm
-PApp : PTm -> PTm -> PTm
-PPair : PTm -> PTm -> PTm
-PProj : PTag -> PTm -> PTm
-PConst : TTag -> PTm
-PUniv : nat -> PTm
-PBot : PTm
-
+PL : PTag
+PR : PTag
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
+Bot : Tm
 Univ : nat -> Tm
-BVal : bool -> Tm
-Bool : Tm
-If : Tm -> Tm -> Tm -> Tm

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/compile.v

@@ -1,186 +0,0 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
-Require Import ssreflect ssrbool.
-From Hammer Require Import Tactics.
-From stdpp Require Import relations (rtc(..)).
-
-Module Compile.
-  Fixpoint F {n} (a : Tm n) : Tm n :=
-    match a with
-    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
-    | Const k => Const k
-    | Univ i => Univ i
-    | Abs a => Abs (F a)
-    | App a b => App (F a) (F b)
-    | VarTm i => VarTm i
-    | Pair a b => Pair (F a) (F b)
-    | Proj t a => Proj t (F a)
-    | Bot => Bot
-    | If a b c => App (App (F a) (F b)) (F c)
-    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
-    | Bool => Bool
-    end.
-
-  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
-    F (ren_Tm ξ a)= ren_Tm ξ (F a).
-  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.
-
-  #[local]Hint Rewrite Compile.renaming : compile.
-
-  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
-    (forall i, ρ0 i = F (ρ1 i)) ->
-    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
-  Proof.
-    move : m ρ0 ρ1. elim : n / a => n//=.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - hauto lq:on.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-  Qed.
-
-  Lemma substing n b (a : Tm (S n)) :
-    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
-  Proof.
-    apply morphing.
-    case => //=.
-  Qed.
-
-End Compile.
-
-#[export] Hint Rewrite Compile.renaming Compile.morphing : compile.
-
-
-Module Join.
-  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).
-
-  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
-    R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
-  Proof.
-    rewrite /R /= !join_pair_inj.
-    move => [[/join_const_inj h0 h1] h2].
-    apply abs_eq in h2.
-    evar (t : Tm (S n)).
-    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
-      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
-    subst t. rewrite -/ren_Tm.
-    move : h2. move /join_transitive => /[apply]. asimpl => h2.
-    tauto.
-  Qed.
-
-  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
-  Proof. hauto l:on use:join_univ_inj. Qed.
-
-  Lemma transitive n (a b c : Tm n) :
-    R a b -> R b c -> R a c.
-  Proof. hauto l:on use:join_transitive unfold:R. Qed.
-
-  Lemma symmetric n (a b : Tm n) :
-    R a b -> R b a.
-  Proof. hauto l:on use:join_symmetric. Qed.
-
-  Lemma reflexive n (a : Tm n) :
-    R a a.
-  Proof. hauto l:on use:join_refl. Qed.
-
-  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
-    R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
-  Proof.
-    rewrite /R.
-    rewrite /join.
-    move => [C [h0 h1]].
-    repeat (rewrite <- Compile.morphing with (ρ0 := funcomp Compile.F ρ); last by reflexivity).
-    hauto lq:on use:join_substing.
-  Qed.
-
-End Join.
-
-Module Equiv.
-  Inductive R {n} : Tm n -> Tm n ->  Prop :=
-  (***************** Beta ***********************)
-  | AppAbs a b :
-    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
-  | ProjPair p a b :
-    R (Proj p (Pair a b)) (if p is PL then a else b)
-
-  (****************** Eta ***********************)
-  | AppEta a :
-    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
-  | PairEta a :
-    R a (Pair (Proj PL a) (Proj PR a))
-
-  (*************** Congruence ********************)
-  | Var i : R (VarTm i) (VarTm i)
-  | AbsCong a b :
-    R a b ->
-    R (Abs a) (Abs b)
-  | AppCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (App a0 b0) (App a1 b1)
-  | PairCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (Pair a0 b0) (Pair a1 b1)
-  | ProjCong p a0 a1 :
-    R a0 a1 ->
-    R (Proj p a0) (Proj p a1)
-  | BindCong p A0 A1 B0 B1:
-    R A0 A1 ->
-    R B0 B1 ->
-    R (TBind p A0 B0) (TBind p A1 B1)
-  | UnivCong i :
-    R (Univ i) (Univ i).
-End Equiv.
-
-Module EquivJoin.
-  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
-  Proof.
-    move => h. elim : n a b /h => n.
-    - move => a b.
-      rewrite /Join.R /join /=.
-      eexists. split. apply relations.rtc_once.
-      apply Par.AppAbs; auto using Par.refl.
-      rewrite Compile.substing.
-      apply relations.rtc_refl.
-    - move => p a b.
-      apply Join.FromPar.
-      simpl. apply : Par.ProjPair'; auto using Par.refl.
-      case : p => //=.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.AppEta'; auto using Par.refl.
-      by autorewrite with compile.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.PairEta; auto using Par.refl.
-    - hauto l:on use:Join.FromPar, Par.Var.
-    - hauto lq:on use:Join.AbsCong.
-    - qauto l:on use:Join.AppCong.
-    - qauto l:on use:Join.PairCong.
-    - qauto use:Join.ProjCong.
-    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
-      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
-    - hauto l:on.
-  Qed.
-End EquivJoin.
-
-Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
-Proof.
-  move => h. elim : n a b /h.
-  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
-    rewrite -Compile.substing.
-    apply RPar'.AppAbs => //.
-  - hauto q:on use:RPar'.ProjPair'.
-  - qauto ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-Qed.
-
-Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
-Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.

theories/diagram.txt

@@ -18,25 +18,3 @@ a0 >> a1
 |     |
 v     v
 b0 >> b1
-
-
-prov x (x, x)
-
-prov x b
-
-
-a => b
-
-prov x a
-
-prov y b
-
-prov x c
-prov y c
-
-extract c = x
-extract c = y
-
-prov x b
-
-pr

theories/logrel.v

@@ -1,26 +1,23 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red compile.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import fp_red.
 From Hammer Require Import Tactics.
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
 Require Import Logic.PropExtensionality (propositional_extensionality).
 From stdpp Require Import relations (rtc(..), rtc_subrel).
 Import Psatz.
-
-Definition ProdSpace {n} (PA : Tm n -> Prop)
-  (PF : Tm n -> (Tm n -> Prop) -> Prop) b : Prop :=
+Definition ProdSpace (PA : Tm 0 -> Prop)
+  (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) b : Prop :=
   forall a PB, PA a -> PF a PB -> PB (App b a).
 
-Definition SumSpace {n} (PA : Tm n -> Prop)
-  (PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop :=
-  wne t \/ exists a b, rtc RPar'.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
+Definition SumSpace (PA : Tm 0 -> Prop)
+  (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop) t : Prop :=
+  exists a b, rtc RPar.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
 
-Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace.
+Definition BindSpace p := if p is TPi then ProdSpace else SumSpace.
 
 Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
-Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop :=
-| InterpExt_Ne A :
-  ne A ->
-  ⟦ A ⟧ i ;; I ↘ wne
+Inductive InterpExt i (I : nat -> Tm 0 -> Prop) : Tm 0 -> (Tm 0 -> Prop) -> Prop :=
 | InterpExt_Bind p A B PA PF :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, PF a PB) ->
@@ -32,12 +29,12 @@ Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) ->
   ⟦ Univ j ⟧ i ;; I ↘ (I j)
 
 | InterpExt_Step A A0 PA :
-  RPar'.R A A0 ->
+  RPar.R A A0 ->
   ⟦ A0 ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PA
 where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
 
-Lemma InterpExt_Univ' n i  I j (PF : Tm n -> Prop) :
+Lemma InterpExt_Univ'  i  I j (PF : Tm 0 -> Prop) :
   PF = I j ->
   j < i ->
   ⟦ Univ j ⟧ i ;; I ↘ PF.
@@ -45,29 +42,28 @@ Proof. hauto lq:on ctrs:InterpExt. Qed.
 
 Infix "<?" := Compare_dec.lt_dec (at level 60).
 
-Equations InterpUnivN n (i : nat) : Tm n -> (Tm n -> Prop) -> Prop by wf i lt :=
-  InterpUnivN n i := @InterpExt n i
+Equations InterpUnivN (i : nat) : Tm 0 -> (Tm 0 -> Prop) -> Prop by wf i lt :=
+  InterpUnivN i := @InterpExt i
                      (fun j A =>
                         match j <? i  with
-                        | left _ => exists PA, InterpUnivN n j A PA
+                        | left _ => exists PA, InterpUnivN  j A PA
                         | right _ => False
                         end).
-Arguments InterpUnivN {n}.
+Arguments InterpUnivN .
 
-Lemma InterpExt_lt_impl n i I I' A (PA : Tm n -> Prop) :
+Lemma InterpExt_lt_impl i I I' A (PA : Tm 0 -> Prop) :
   (forall j, j < i -> I j = I' j) ->
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I' ↘ PA.
 Proof.
   move => hI h.
   elim : A PA /h.
-  - hauto q:on ctrs:InterpExt.
   - hauto lq:on rew:off ctrs:InterpExt.
   - hauto q:on ctrs:InterpExt.
   - hauto lq:on ctrs:InterpExt.
 Qed.
 
-Lemma InterpExt_lt_eq n i I I' A (PA : Tm n -> Prop) :
+Lemma InterpExt_lt_eq i I I' A (PA : Tm 0 -> Prop) :
   (forall j, j < i -> I j = I' j) ->
   ⟦ A ⟧ i ;; I ↘ PA =
   ⟦ A ⟧ i ;; I' ↘ PA.
@@ -79,8 +75,8 @@ Qed.
 
 Notation "⟦ A ⟧ i ↘ S" := (InterpUnivN i A S) (at level 70).
 
-Lemma InterpUnivN_nolt n i :
-  @InterpUnivN n i = @InterpExt n i (fun j (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA).
+Lemma InterpUnivN_nolt i :
+  InterpUnivN i = InterpExt i (fun j (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA).
 Proof.
   simp InterpUnivN.
   extensionality A. extensionality PA.
@@ -93,12 +89,12 @@ Qed.
 #[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
 
 Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n):
-    RPar'.R a b -> RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
-  Proof. hauto l:on inv:option use:RPar'.substing, RPar'.refl. Qed.
+    RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
+  Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed.
 
-Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P
+Lemma InterpExt_Bind_inv p i I (A : Tm 0) B P
   (h :  ⟦ TBind p A B ⟧ i ;; I ↘ P) :
-  exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
+  exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, PF a PB) /\
     (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
@@ -107,35 +103,24 @@ Proof.
   move E : (TBind p A B) h => T h.
   move : A B E.
   elim : T P / h => //.
-  - move => //= *. scongruence.
   - hauto l:on.
   - move => A A0 PA hA hA0 hPi A1 B ?. subst.
-    elim /RPar'.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
+    elim /RPar.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
     hauto lq:on ctrs:InterpExt use:RPar_substone.
 Qed.
 
-Lemma InterpExt_Ne_inv n i A I P
-  (h :  ⟦ A : Tm n  ⟧ i ;; I ↘ P) :
-  ne A ->
-  P = wne.
-Proof.
-  elim : A P / h => //=.
-  qauto l:on ctrs:prov inv:prov use:nf_refl.
-Qed.
-
-Lemma InterpExt_Univ_inv n i I j P
-  (h :  ⟦ Univ j : Tm n  ⟧ i ;; I ↘ P) :
+Lemma InterpExt_Univ_inv i I j P
+  (h :  ⟦ Univ j  ⟧ i ;; I ↘ P) :
   P = I j /\ j < i.
 Proof.
   move : h.
   move E : (Univ j) => T h. move : j E.
   elim : T P /h => //.
-  - move => //= *. scongruence.
   - hauto l:on.
-  - hauto lq:on rew:off inv:RPar'.R.
+  - hauto lq:on rew:off inv:RPar.R.
 Qed.
 
-Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA  :
+Lemma InterpExt_Bind_nopf p i I (A : Tm 0) B PA  :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘  PB) ->
   ⟦ TBind p A B ⟧ i ;; I ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB)).
@@ -143,7 +128,7 @@ Proof.
   move => h0 h1. apply InterpExt_Bind =>//.
 Qed.
 
-Lemma InterpUnivN_Fun_nopf n p i (A : Tm n) B PA :
+Lemma InterpUnivN_Fun_nopf p i (A : Tm 0) B PA :
   ⟦ A ⟧ i ↘ PA ->
   (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) ->
   ⟦ TBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB)).
@@ -151,7 +136,7 @@ Proof.
   hauto l:on use:InterpExt_Bind_nopf rew:db:InterpUniv.
 Qed.
 
-Lemma InterpExt_cumulative n i j I (A : Tm n) PA :
+Lemma InterpExt_cumulative i j I (A : Tm 0) PA :
   i <= j ->
    ⟦ A ⟧ i ;; I ↘ PA ->
    ⟦ A ⟧ j ;; I ↘ PA.
@@ -161,87 +146,61 @@ Proof.
     hauto l:on ctrs:InterpExt solve+:(by lia).
 Qed.
 
-Lemma InterpUnivN_cumulative n i (A : Tm n) PA :
+Lemma InterpUnivN_cumulative i (A : Tm 0) PA :
    ⟦ A ⟧ i ↘ PA -> forall j, i <= j ->
    ⟦ A ⟧ j ↘ PA.
 Proof.
   hauto l:on rew:db:InterpUniv use:InterpExt_cumulative.
 Qed.
 
-Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) :
-  RPar'.R A B ->
+Lemma InterpExt_preservation i I (A : Tm 0) B P (h : InterpExt i I A P) :
+  RPar.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof.
   move : B.
   elim : A P / h; auto.
-  - hauto lq:on use:nf_refl ctrs:InterpExt.
   - move => p A B PA PF hPA ihPA hPB hPB' ihPB T hT.
-    elim /RPar'.inv :  hT => //.
+    elim /RPar.inv :  hT => //.
     move => hPar p0 A0 A1 B0 B1 h0 h1 [? ?] ? ?; subst.
     apply InterpExt_Bind; auto => a PB hPB0.
     apply : ihPB; eauto.
-    sfirstorder use:RPar'.cong, RPar'.refl.
-  - hauto lq:on inv:RPar'.R ctrs:InterpExt.
+    sfirstorder use:RPar.cong, RPar.refl.
+  - hauto lq:on inv:RPar.R ctrs:InterpExt.
   - move => A B P h0 h1 ih1 C hC.
-    have [D [h2 h3]] := RPar'_diamond  _ _ _ _ h0 hC.
+    have [D [h2 h3]] := RPar_diamond  _ _ _ _ h0 hC.
     hauto lq:on ctrs:InterpExt.
 Qed.
 
-Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
-  RPar'.R A B ->
+Lemma InterpUnivN_preservation i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) :
+  RPar.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed.
 
-Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
-  rtc RPar'.R A B ->
+Lemma InterpExt_back_preservation_star i I (A : Tm 0) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
+  rtc RPar.R A B ->
   ⟦ A ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on ctrs:InterpExt. Qed.
 
-Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
-  rtc RPar'.R A B ->
+Lemma InterpExt_preservation_star i I (A : Tm 0) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
+  rtc RPar.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed.
 
-Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
-  rtc RPar'.R A B ->
+Lemma InterpUnivN_preservation_star i (A : Tm 0) B P (h : ⟦ A ⟧ i ↘ P) :
+  rtc RPar.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed.
 
-Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) :
-  rtc RPar'.R A B ->
+Lemma InterpUnivN_back_preservation_star i (A : Tm 0) B P (h : ⟦ B ⟧ i ↘ P) :
+  rtc RPar.R A B ->
   ⟦ A ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed.
 
-Function hfb {n} (A : Tm n) :=
-  match A with
-  | TBind _ _ _ => true
-  | Univ _ => true
-  | _ => ne A
-  end.
-
-Inductive hfb_case {n} : Tm n -> Prop :=
-| hfb_bind p A B :
-  hfb_case (TBind p A B)
-| hfb_univ i :
-  hfb_case (Univ i)
-| hfb_ne A :
-  ne A ->
-  hfb_case A.
-
-Derive Dependent Inversion hfb_inv with (forall n (a : Tm n), hfb_case a) Sort Prop.
-
-Lemma ne_hfb {n} (A : Tm n) : ne A -> hfb A.
-Proof. case : A => //=. Qed.
-
-Lemma hfb_caseP {n} (A : Tm n) : hfb A -> hfb_case A.
-Proof. hauto lq:on ctrs:hfb_case inv:Tm use:ne_hfb. Qed.
-
-Lemma InterpExtInv n i I (A : Tm n) PA :
+Lemma InterpExtInv i I (A : Tm 0) PA :
   ⟦ A ⟧ i ;; I ↘ PA ->
-  exists B, hfb B /\ rtc RPar'.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
+  exists B, hfb B /\ rtc RPar.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
 Proof.
   move => h. elim : A PA /h.
-  - hauto q:on ctrs:InterpExt, rtc use:ne_hfb.
   - move => p A B PA PF hPA _ hPF hPF0 _.
     exists (TBind p A B). repeat split => //=.
     apply rtc_refl.
@@ -251,26 +210,17 @@ Proof.
   - hauto lq:on ctrs:rtc.
 Qed.
 
-Lemma RPar'_Par n (A B : Tm n) :
-  RPar'.R A B ->
-  Par.R A B.
-Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.
-
-Lemma RPar's_Pars n (A B : Tm n) :
-  rtc RPar'.R A B ->
+Lemma RPars_Pars  (A B : Tm 0) :
+  rtc RPar.R A B ->
   rtc Par.R A B.
-Proof. hauto lq:on use:RPar'_Par, rtc_subrel. Qed.
+Proof. hauto lq:on use:RPar_Par, rtc_subrel. Qed.
 
-Lemma RPar's_join n (A B : Tm n) :
-  rtc RPar'.R A B -> Join.R A B.
-Proof.
-  rewrite /Join.R => h.
-  have {}h : rtc RPar'.R (Compile.F A) (Compile.F B) by eauto using compile_rpars.
-  rewrite /join. eauto using RPar's_Pars, rtc_refl.
-Qed.
+Lemma RPars_join  (A B : Tm 0) :
+  rtc RPar.R A B -> join A B.
+Proof. hauto lq:on ctrs:rtc use:RPars_Pars. Qed.
 
-Lemma bindspace_iff n p (PA : Tm n -> Prop) PF PF0 b  :
-  (forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
+Lemma bindspace_iff  p (PA : Tm 0 -> Prop) PF PF0 b  :
+  (forall (a : Tm 0) (PB PB0 : Tm 0 -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
   (forall a, PA a -> exists PB, PF a PB) ->
   (forall a, PA a -> exists PB0, PF0 a PB0) ->
   (BindSpace p PA PF b <-> BindSpace p PA PF0 b).
@@ -291,105 +241,23 @@ Proof.
     hauto lq:on rew:off.
 Qed.
 
-Lemma ne_prov_inv n (a : Tm n) :
-  ne a -> (exists i, prov (VarTm i) a) \/ prov Bot a.
-Proof.
-  elim : n /a => //=.
-  - hauto lq:on ctrs:prov.
-  - hauto lq:on rew:off ctrs:prov b:on.
-  - hauto lq:on ctrs:prov.
-  - move => n k.
-    have : @prov n Bot Bot by auto using P_Bot.
-    eauto.
-Qed.
-
-Lemma ne_pars_inv n (a b : Tm n) :
-  ne a -> rtc Par.R a b -> (exists i, prov (VarTm i) b) \/ prov Bot b.
-Proof.
-  move /ne_prov_inv.
-  sfirstorder use:prov_pars.
-Qed.
-
-Lemma ne_pars_extract  n (a b : Tm n) :
-  ne a -> rtc Par.R a b -> (exists i, extract b = (VarTm i)) \/ extract b = Bot.
-Proof. hauto lq:on rew:off use:ne_pars_inv, prov_extract. Qed.
-
-Lemma const_pars_extract n k b :
-  rtc Par.R (Const k : Tm n) b -> extract b = Const k.
-Proof. hauto l:on use:pars_const_inv, prov_extract. Qed.
-
-Lemma compile_ne n (a : Tm n) :
-  ne a = ne (Compile.F a) /\ nf a = nf (Compile.F a).
-Proof.
-  elim : n / a => //=; sfirstorder b:on.
-Qed.
-
-Lemma join_univ_pi_contra n p (A : Tm n) B i :
-  Join.R (TBind p A B) (Univ i) -> False.
-Proof.
-  rewrite /Join.R /=.
-  rewrite !pair_eq.
-  move => [[h _ ]_ ].
-  move : h => [C [h0 h1]].
-  have ?  : extract C = Const p by hauto l:on use:pars_const_inv.
-  have h : prov (Univ i : Tm n) (Proj PL (Proj PL (Univ i))) by hauto lq:on ctrs:prov.
-  have {h} : prov (Univ i) C by eauto using prov_pars.
-  move /prov_extract=>/=. congruence.
-Qed.
-
-Lemma join_bind_ne_contra n p (A : Tm n) B C :
-  ne C ->
-  Join.R (TBind p A B) C -> False.
-Proof.
-  rewrite /Join.R. move => hC /=.
-  rewrite !pair_eq.
-  move => [[[D [h0 h1]] _] _].
-  have {}hC : ne (Compile.F C) by hauto lq:on use:compile_ne.
-  have {}hC : ne (Proj PL (Proj PL (Compile.F C))) by scongruence.
-  have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
-  have : extract D = Const p by eauto using const_pars_extract.
-  sfirstorder.
-Qed.
-
-Lemma join_univ_ne_contra n i C :
-  ne C ->
-  Join.R (Univ i : Tm n) C -> False.
-Proof.
-  move => hC [D [h0 h1]].
-  move /pars_univ_inv : h0 => ?.
-  have : (exists i, extract D = (VarTm i)) \/ exists k, extract D =(Const k)  by hauto q:on use:ne_pars_extract, compile_ne.
-  sfirstorder.
-Qed.
-
-#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra Join.symmetric Join.transitive : join.
-
-Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
+Lemma InterpExt_Join i I (A B : Tm 0) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ B ⟧ i ;; I ↘ PB ->
-  Join.R A B ->
+  join A B ->
   PA = PB.
 Proof.
   move => h. move : B PB. elim : A PA /h.
-  - move => A hA B PB /InterpExtInv.
-    move => [B0 []].
-    move /hfb_caseP. elim/hfb_inv => _.
-    + move => p A0 B1 ? [/RPar's_join h0 h1] h2. subst. exfalso.
-      eauto with join.
-    + move => ? ? [/RPar's_join *]. subst. exfalso.
-      eauto with join.
-    + hauto lq:on use:InterpExt_Ne_inv.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF U PU /InterpExtInv.
     move => [B0 []].
-    move /hfb_caseP.
-    elim /hfb_inv => _.
-    rename B0 into B00.
-    + move => p0 A0 B0 ?  [hr hPi]. subst.
+    case : B0 => //=.
+    + move => p0 A0 B0 _ [hr hPi].
       move /InterpExt_Bind_inv : hPi.
       move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst.
       move => hjoin.
-      have{}hr : Join.R U (TBind p0 A0 B0) by auto using RPar's_join.
-      have hj : Join.R (TBind p A B) (TBind p0 A0 B0) by eauto using Join.transitive.
-      have {hj} : p0 = p /\ Join.R A A0 /\ Join.R B B0 by hauto l:on use:Join.BindInj.
+      have{}hr : join U (TBind p0 A0 B0) by auto using RPars_join.
+      have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive.
+      have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj.
       move => [? [h0 h1]]. subst.
       have ? : PA0 = PA by hauto l:on. subst.
       rewrite /ProdSpace.
@@ -398,70 +266,66 @@ Proof.
       apply bindspace_iff; eauto.
       move => a PB PB0 hPB hPB0.
       apply : ihPF; eauto.
-      rewrite /Join.R.
-      rewrite -!Compile.substing.
-      hauto l:on use:join_substing.
-    + move => j ?. subst.
+      by apply join_substing.
+    + move => j _.
       move => [h0 h1] h.
-      have ? : Join.R U (Univ j) by eauto using RPar's_join.
-      have : Join.R (TBind p A B) (Univ j) by eauto using Join.transitive.
+      have ? : join U (Univ j) by eauto using RPars_join.
+      have : join (TBind p A B) (Univ j) by eauto using join_transitive.
       move => ?. exfalso.
-      hauto l: on use: join_univ_pi_contra.
-    + move => A0 ? ? [/RPar's_join ?]. subst.
-      move => _ ?. exfalso. eauto with join.
+      eauto using join_univ_pi_contra.
   - move => j ? B PB /InterpExtInv.
-    move => [? []]. move/hfb_caseP.
-    elim /hfb_inv => //= _.
+    move => [+ []]. case => //=.
     + move => p A0 B0 _ [].
-      move /RPar's_join => *.
-      exfalso. eauto with join.
-    + move => m _ [/RPar's_join h0 + h1].
-      have /join_univ_inj {h0 h1} ?  : Join.R (Univ j : Tm n) (Univ m) by eauto using Join.transitive.
+      move /RPars_join => *.
+      have ?  : join (TBind p A0 B0) (Univ j) by eauto using join_symmetric, join_transitive.
+      exfalso.
+      eauto using join_univ_pi_contra.
+    + move => m _ [/RPars_join h0 + h1].
+      have /join_univ_inj {h0 h1} ?  : join (Univ j : Tm 0) (Univ m) by eauto using join_transitive.
       subst.
       move /InterpExt_Univ_inv. firstorder.
-    + move => A ? ? [/RPar's_join] *. subst. exfalso. eauto with join.
   - move => A A0 PA h.
-    have /Join.symmetric {}h : Join.R A A0 by hauto lq:on ctrs:rtc use:RPar's_join, relations.rtc_once.
-    eauto with join.
+    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar_Par, relations.rtc_once.
+    eauto using join_transitive.
 Qed.
 
-Lemma InterpUniv_Join n i (A B : Tm n) PA PB :
+Lemma InterpUniv_Join i (A B : Tm 0) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ i ↘ PB ->
-  Join.R A B ->
+  join A B ->
   PA = PB.
 Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Bind_inv n p i  (A : Tm n) B P
+Lemma InterpUniv_Bind_inv p i  (A : Tm 0) B P
   (h :  ⟦ TBind p A B ⟧ i ↘ P) :
-  exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
+  exists (PA : Tm 0 -> Prop) (PF : Tm 0 -> (Tm 0 -> Prop) -> Prop),
      ⟦ A ⟧ i ↘ PA /\
     (forall a, PA a -> exists PB, PF a PB) /\
     (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
     P = BindSpace p PA PF.
 Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Univ_inv n i j P
+Lemma InterpUniv_Univ_inv i j P
   (h :  ⟦ Univ j  ⟧ i ↘ P) :
-  P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
+  P = (fun (A : Tm 0) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
 Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_Functional n i I (A B : Tm n) PA PB :
+Lemma InterpExt_Functional i I (A B : Tm 0) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Join, join_refl. Qed.
 
-Lemma InterpUniv_Functional n i (A : Tm n) PA PB :
+Lemma InterpUniv_Functional i (A : Tm 0) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ A ⟧ i ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Join' n i j (A B : Tm n) PA PB :
+Lemma InterpUniv_Join' i j (A B : Tm 0) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ j ↘ PB ->
-  Join.R A B ->
+  join A B ->
   PA = PB.
 Proof.
   have [? ?] : i <= max i j /\ j <= max i j by lia.
@@ -471,16 +335,16 @@ Proof.
   eauto using InterpUniv_Join.
 Qed.
 
-Lemma InterpUniv_Functional' n i j A PA PB :
-  ⟦ A : Tm n ⟧ i ↘ PA ->
+Lemma InterpUniv_Functional' i j A PA PB :
+  ⟦ A ⟧ i ↘ PA ->
   ⟦ A ⟧ j ↘ PB ->
   PA = PB.
 Proof.
   hauto l:on use:InterpUniv_Join', join_refl.
 Qed.
 
-Lemma InterpExt_Bind_inv_nopf i n I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
-  exists (PA : Tm n -> Prop),
+Lemma InterpExt_Bind_inv_nopf i I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
+  exists (PA : Tm 0 -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
       P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB).
@@ -501,42 +365,34 @@ Proof.
       split; hauto q:on use:InterpExt_Functional.
 Qed.
 
-Lemma InterpUniv_Bind_inv_nopf n i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
-  exists (PA : Tm n -> Prop),
+Lemma InterpUniv_Bind_inv_nopf i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
+  exists (PA : Tm 0 -> Prop),
      ⟦ A ⟧ i ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
       P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB).
 Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_back_clos n i I (A : Tm n) PA :
-  (forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a) ->
+Lemma InterpExt_back_clos i I (A : Tm 0) PA :
+  (forall j,  forall a b, (RPar.R a b) ->  I j b -> I j a) ->
     ⟦ A ⟧ i ;; I ↘ PA ->
-    forall a b, (RPar'.R a b) ->
+    forall a b, (RPar.R a b) ->
            PA b -> PA a.
 Proof.
   move => hI h.
   elim : A PA /h.
-  - hauto q:on ctrs:rtc unfold:wne.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
     case : p => //=.
-    + have  : forall b0 b1 a, RPar'.R b0 b1 -> RPar'.R (App b0 a) (App b1 a)
-          by hauto lq:on ctrs:RPar'.R use:RPar'.refl.
+    + have  : forall b0 b1 a, RPar.R b0 b1 -> RPar.R (App b0 a) (App b1 a)
+          by hauto lq:on ctrs:RPar.R use:RPar.refl.
       hauto lq:on rew:off unfold:ProdSpace.
     + hauto lq:on ctrs:rtc unfold:SumSpace.
   - eauto.
   - eauto.
 Qed.
 
-Lemma InterpExt_back_clos_star n i I (A : Tm n) PA :
-  (forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a) ->
-    ⟦ A ⟧ i ;; I ↘ PA ->
-    forall a b, (rtc RPar'.R a b) ->
-           PA b -> PA a.
-Proof. induction 3; hauto l:on use:InterpExt_back_clos. Qed.
-
-Lemma InterpUniv_back_clos n i (A : Tm n) PA :
+Lemma InterpUniv_back_clos i (A : Tm 0) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, (RPar'.R a b) ->
+    forall a b, (RPar.R a b) ->
            PA b -> PA a.
 Proof.
   simp InterpUniv.
@@ -544,9 +400,9 @@ Proof.
   hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
 Qed.
 
-Lemma InterpUniv_back_clos_star n i (A : Tm n) PA :
+Lemma InterpUniv_back_clos_star i (A : Tm 0) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, rtc RPar'.R a b ->
+    forall a b, rtc RPar.R a b ->
            PA b -> PA a.
 Proof.
   move => h  a b.
@@ -554,101 +410,30 @@ Proof.
   hauto lq:on use:InterpUniv_back_clos.
 Qed.
 
-Lemma pars'_wn {n} a b :
-  rtc RPar'.R a b ->
-  @wn n b ->
-  wn a.
-Proof. sfirstorder unfold:wn use:@relations.rtc_transitive. Qed.
+Definition ρ_ok {n} Γ (ρ : fin n -> Tm 0) := forall i m PA,
+  ⟦ subst_Tm ρ (Γ i) ⟧ m ↘ PA -> PA (ρ i).
 
-(* P identifies a set of "reducibility candidates" *)
-Definition CR {n} (P : Tm n -> Prop) :=
-  (forall a, P a -> wn a) /\
-    (forall a, ne a -> P a).
-
-Lemma adequacy_ext i n I A PA
-  (hI0 : forall j,  j < i -> forall a b, (RPar'.R a b) ->  I j b -> I j a)
-  (hI : forall j, j < i -> CR (I j))
-  (h :  ⟦ A : Tm n ⟧ i ;; I ↘ PA) :
-  CR PA /\ wn A.
-Proof.
-  elim : A PA / h.
-  - hauto unfold:wne use:wne_wn.
-  - move => p A B PA PF hA hPA hTot hRes ihPF.
-    rewrite /CR.
-    have hb : PA Bot by firstorder.
-    repeat split.
-    + case : p => /=.
-      * qauto l:on use:ext_wn unfold:ProdSpace, CR.
-      * rewrite /SumSpace => a []; first by eauto with nfne.
-        move => [q0][q1]*.
-        have : wn q0 /\ wn q1 by hauto q:on.
-        qauto l:on use:wn_pair, pars'_wn.
-    + case : p => /=.
-      * rewrite /ProdSpace.
-        move => a ha c PB hc hPB.
-        have hc' : wn c by sfirstorder.
-        have : wne (App a c) by hauto lq:on use:wne_app ctrs:rtc.
-        have h : (forall a, ne a -> PB a) by sfirstorder.
-        suff : (forall a, wne a -> PB a) by hauto l:on.
-        move => a0 [a1 [h0 h1]].
-        eapply InterpExt_back_clos_star with (b := a1); eauto.
-      * rewrite /SumSpace.
-        move => a ha. left.
-        sfirstorder ctrs:rtc.
-    + have wnA : wn A by firstorder.
-      apply wn_bind => //.
-      apply wn_antirenaming with (ρ := scons Bot VarTm);first by  hauto q:on inv:option.
-      hauto lq:on.
-  - hauto l:on.
-  - hauto lq:on rew:off ctrs:rtc.
-Qed.
-
-Lemma adequacy i n A PA
-  (h :  ⟦ A : Tm n ⟧ i ↘ PA) :
-  CR PA /\ wn A.
-Proof.
-  move : i A PA h.
-  elim /Wf_nat.lt_wf_ind => i ih A PA.
-  simp InterpUniv.
-  apply adequacy_ext.
-  hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
-  hauto l:on use:InterpExt_Ne rew:db:InterpUniv.
-Qed.
-
-Lemma adequacy_wne i n A PA a : ⟦ A : Tm n ⟧ i ↘ PA -> wne a -> PA a.
-Proof. qauto l:on use:InterpUniv_back_clos_star, adequacy unfold:CR. Qed.
-
-Lemma adequacy_wn i n A PA (h :  ⟦ A : Tm n ⟧ i ↘ PA) a : PA a -> wn a.
-Proof. hauto q:on use:adequacy. Qed.
-
-Definition ρ_ok {n} (Γ : fin n -> Tm n) (ρ : fin n -> Tm 0) := forall i k PA,
-  ⟦ subst_Tm ρ (Γ i) ⟧ k ↘ PA -> PA (ρ i).
-
-Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_Tm ρ A ⟧ k ↘ PA /\ PA (subst_Tm ρ a).
+Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists m PA, ⟦ subst_Tm ρ A ⟧ m ↘ PA /\ PA (subst_Tm ρ a).
 Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
 
 (* Semantic context wellformedness *)
 Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ Univ j.
 Notation "⊨ Γ" := (SemWff Γ) (at level 70).
 
-Lemma ρ_ok_bot n (Γ : fin n -> Tm n)  :
-  ρ_ok Γ (fun _ => Bot).
-Proof.
-  rewrite /ρ_ok.
-  hauto q:on use:adequacy.
-Qed.
+Lemma ρ_ok_nil ρ :
+  ρ_ok null ρ.
+Proof.  rewrite /ρ_ok. inversion i; subst. Qed.
 
 Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A :
   ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->
   ρ_ok Γ ρ ->
-  ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) (scons a ρ).
+  ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) ((scons a ρ)).
 Proof.
   move => h0 h1 h2.
   rewrite /ρ_ok.
   move => j.
   destruct j as [j|].
   - move => m PA0. asimpl => ?.
-    asimpl.
     firstorder.
   - move => m PA0. asimpl => h3.
     have ? : PA0 = PA by eauto using InterpUniv_Functional'.
@@ -670,7 +455,7 @@ Proof.
   rewrite /ρ_ok in hρ.
   move => h.
   rewrite /funcomp.
-  apply hρ with (k := m').
+  apply hρ with (m := m').
   move : h. rewrite -hξ.
   by asimpl.
 Qed.
@@ -695,17 +480,6 @@ Proof.
   hauto lq:on inv:option unfold:renaming_ok.
 Qed.
 
-Lemma SemWt_Wn n Γ (a : Tm n) A :
-  Γ ⊨ a ∈ A ->
-  wn a /\ wn A.
-Proof.
-  move => h.
-  have {}/h := ρ_ok_bot _ Γ => h.
-  have h0 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) A) by hauto l:on use:adequacy.
-  have h1 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) a)by hauto l:on use:adequacy_wn.
-  move {h}. hauto lq:on use:wn_antirenaming.
-Qed.
-
 Lemma SemWt_Univ n Γ (A : Tm n) i  :
   Γ ⊨ A ∈ Univ i <->
   forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_Tm ρ A ⟧ i ↘ S.
@@ -768,12 +542,12 @@ Qed.
 Lemma ST_Conv n Γ (a : Tm n) A B i :
   Γ ⊨ a ∈ A ->
   Γ ⊨ B ∈ Univ i ->
-  Join.R A B ->
+  join A B ->
   Γ ⊨ a ∈ B.
 Proof.
   move => ha /SemWt_Univ h h0.
   move => ρ hρ.
-  have {}h0 : Join.R (subst_Tm ρ A) (subst_Tm ρ B) by eauto using Join.substing.
+  have {}h0 : join (subst_Tm ρ A) (subst_Tm ρ B) by eauto using join_substing.
   move /ha : (hρ){ha} => [m [PA [h1 h2]]].
   move /h : (hρ){h} => [S hS].
   have ? : PA = S by eauto using InterpUniv_Join'. subst.
@@ -798,7 +572,7 @@ Proof.
   intros (m & PB0 & hPB0 & hPB0').
   replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'.
   apply : InterpUniv_back_clos; eauto.
-  apply : RPar'.AppAbs'; eauto using RPar'.refl.
+  apply : RPar.AppAbs'; eauto using RPar.refl.
   by asimpl.
 Qed.
 
@@ -830,7 +604,7 @@ Proof.
   simpl in hPPi.
   move /InterpUniv_Bind_inv_nopf : hPPi.
   move => [PA [hPA [hTot ?]]]. subst=>/=.
-  rewrite /SumSpace. right.
+  rewrite /SumSpace.
   exists (subst_Tm ρ a), (subst_Tm ρ b).
   split.
   - hauto l:on use:Pars.substing.
@@ -852,25 +626,24 @@ Proof.
   move : h0 => [S][h2][h3]?. subst.
   move : h1 => /=.
   rewrite /SumSpace.
-  case; first by hauto lq:on use:adequacy_wne, wne_proj.
   move => [a0 [b0 [h4 [h5 h6]]]].
   exists m, S. split => //=.
-  have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars'.ProjCong.
-  have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'.
-  have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+  have {}h4 : rtc RPar.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars.ProjCong.
+  have ? : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.refl, RPar.ProjPair'.
+  have : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
   move => h.
   apply : InterpUniv_back_clos_star; eauto.
 Qed.
 
-Lemma substing_RPar' n m (A : Tm (S n)) ρ (B : Tm m) C :
-  RPar'.R B C ->
-  RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. hauto lq:on inv:option use:RPar'.morphing, RPar'.refl. Qed.
+Lemma substing_RPar n m (A : Tm (S n)) ρ (B : Tm m) C :
+  RPar.R B C ->
+  RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. hauto lq:on inv:option use:RPar.morphing, RPar.refl. Qed.
 
-Lemma substing_RPar's n m (A : Tm (S n)) ρ (B : Tm m) C :
-  rtc RPar'.R B C ->
-  rtc RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar'. Qed.
+Lemma substing_RPars n m (A : Tm (S n)) ρ (B : Tm m) C :
+  rtc RPar.R B C ->
+  rtc RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar. Qed.
 
 Lemma ST_Proj2 n Γ (a : Tm n) A B :
   Γ ⊨ a ∈ TBind TSig A B ->
@@ -881,156 +654,17 @@ Proof.
   move : h0 => [S][h2][h3]?. subst.
   move : h1 => /=.
   rewrite /SumSpace.
-  case.
-  - move => h.
-    have hp : forall p, wne (Proj p (subst_Tm ρ a)) by auto using wne_proj.
-    have hp0 := hp PL. have hp1 := hp PR => {hp}.
-    have : S (Proj PL (subst_Tm ρ a)) by hauto q:on use:adequacy_wne.
-    move /h3 => [PB]. asimpl. hauto lq:on use:adequacy_wne.
-  - move => [a0 [b0 [h4 [h5 h6]]]].
-    specialize h3 with (1 := h5).
-    move : h3 => [PB hPB].
-    have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars'.ProjCong.
-    have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
-    have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
-    exists m, PB.
-    asimpl. split.
-    + have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
-      have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's.
-      move : hPB. asimpl.
-      eauto using InterpUnivN_back_preservation_star.
-    + hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
+  move => [a0 [b0 [h4 [h5 h6]]]].
+  specialize h3 with (1 := h5).
+  move : h3 => [PB hPB].
+  have hr : forall p, rtc RPar.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars.ProjCong.
+  have hrl : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.ProjPair', RPar.refl.
+  have hrr : RPar.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar.ProjPair', RPar.refl.
+  exists m, PB.
+  asimpl. split.
+  - have h : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+    have {}h : rtc RPar.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPars.
+    move : hPB. asimpl.
+    eauto using InterpUnivN_back_preservation_star.
+  - hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
 Qed.
-
-Lemma ne_nf_preservation n (a b : Tm n) : ERed.R b a -> (ne a -> ne b) /\ (nf a -> nf b).
-Proof.
-  move => h. elim : n b a /h => //=.
-  - move => n a.
-    split => //=.
-    hauto lqb:on use:ne_nf_ren db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-  - hauto lqb:on db:nfne.
-Qed.
-
-Fixpoint size_tm {n} (a : Tm n) :=
-  match a with
-  | VarTm _ => 1
-  | TBind _ A B => 1 + Nat.add (size_tm A) (size_tm B)
-  | Abs a => 1 + size_tm a
-  | App a b => 1 + Nat.add (size_tm a) (size_tm b)
-  | Proj p a => 1 + size_tm a
-  | Pair a b => 1 + Nat.add (size_tm a) (size_tm b)
-  | Bot => 1
-  | Const _ => 1
-  | Univ _ => 1
-  end.
-
-Lemma size_tm_ren n m (ξ : fin n -> fin m) a : size_tm (ren_Tm ξ a) = size_tm a.
-Proof.
-  move : m ξ. elim : n / a => //=; scongruence.
-Qed.
-
-#[export]Hint Rewrite size_tm_ren : size_tm.
-
-Lemma size_η_lt n (a b : Tm n) :
-  ERed.R b a ->
-  size_tm b < size_tm a.
-Proof.
-  move => h. elim : b a / h => //=; hauto l:on rew:db:size_tm.
-Qed.
-
-Lemma ered_local_confluence n (a b c : Tm n) :
-  ERed.R b a ->
-  ERed.R c a ->
-  exists d, rtc ERed.R d b  /\ rtc ERed.R d c.
-Proof.
-  move => h. move : c.
-  elim : n b a / h => n.
-  - move => a c.
-    elim /ERed.inv => //= _.
-    + move => ? ? [*]. subst.
-      have : subst_Tm (scons Bot VarTm) (ren_Tm shift c) = (subst_Tm (scons Bot VarTm) (ren_Tm shift a))
-        by congruence.
-      asimpl => ?. subst.
-      eauto using rtc_refl.
-    + move => a0 a1 ha ? [*]. subst.
-      elim /ERed.inv : ha => //= _.
-      * move => a1 a2 b0 ha ? [*]. subst.
-        have [a2 [h0 h1]] : exists a2, ERed.R a2 a /\ a1 = ren_Tm shift a2 by admit. subst.
-        eexists. split; cycle 1.
-        apply : relations.rtc_r; cycle 1.
-        apply ERed.AppEta.
-        apply rtc_refl.
-        eauto using relations.rtc_once.
-      * hauto q:on ctrs:rtc, ERed.R inv:ERed.R.
-  - move => a c ha.
-    elim /ERed.inv : ha => //= _.
-    + hauto l:on.
-    + move => a0 a1 b0 ha ? [*]. subst.
-      elim /ERed.inv : ha => //= _.
-      move => p a1 a2 ha ? [*]. subst.
-      exists a1. split. by apply relations.rtc_once.
-      apply : rtc_l. apply ERed.PairEta.
-      apply : rtc_l. apply ERed.PairCong1. eauto using ERed.ProjCong.
-      apply rtc_refl.
-    + move => a0 b0 b1 ha ? [*]. subst.
-      elim /ERed.inv : ha => //= _ p a0 a1 h ? [*]. subst.
-      exists a0. split; first by apply relations.rtc_once.
-      apply : rtc_l; first by apply ERed.PairEta.
-      apply relations.rtc_once.
-      hauto lq:on ctrs:ERed.R.
-  - move => a0 a1 ha iha c.
-    elim /ERed.inv => //= _.
-    + move => a2 ? [*]. subst.
-      elim /ERed.inv : ha => //=_.
-      * move => a1 a2 b0 ha ? [*] {iha}. subst.
-        have [a0 [h0 h1]] : exists a0, ERed.R a0 c /\ a1 = ren_Tm shift a0 by admit. subst.
-        exists a0. split; last by apply relations.rtc_once.
-        apply relations.rtc_once. apply ERed.AppEta.
-      * hauto q:on inv:ERed.R.
-    + hauto l:on use:EReds.AbsCong.
-  - move => a0 a1 b ha iha c.
-    elim /ERed.inv => //= _.
-    + hauto lq:on ctrs:rtc use:EReds.AppCong.
-    + hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
-  - move => a b0 b1 hb ihb c.
-    elim /ERed.inv => //=_.
-    + move => a0 a1 a2 ha ? [*]. subst.
-      move {ihb}. exists (App a0 b0).
-      hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
-    + hauto lq:on ctrs:rtc use:EReds.AppCong.
-  - move => a0 a1 b ha iha c.
-    elim /ERed.inv => //= _.
-    + move => ? ?[*]. subst.
-      elim /ERed.inv : ha => //= _ p a1 a2 h ? [*]. subst.
-      exists a1. split; last by apply relations.rtc_once.
-      apply : rtc_l. apply ERed.PairEta.
-      apply relations.rtc_once. hauto lq:on ctrs:ERed.R.
-    + hauto lq:on ctrs:rtc use:EReds.PairCong.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-  - move => a b0 b1 hb hc c. elim /ERed.inv => //= _.
-    + move => ? ? [*]. subst.
-      elim /ERed.inv : hb => //= _ p a0 a1 ha ? [*]. subst.
-      move {hc}.
-      exists a0. split; last by apply relations.rtc_once.
-      apply : rtc_l; first by apply ERed.PairEta.
-      hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-    + hauto lq:on ctrs:rtc use:EReds.PairCong.
-  - qauto l:on inv:ERed.R use:EReds.ProjCong.
-  - move => p A0 A1 B hA ihA.
-    move => c. elim/ERed.inv => //=.
-    + hauto lq:on ctrs:rtc use:EReds.BindCong.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-  - move => p A B0 B1 hB ihB c.
-    elim /ERed.inv => //=.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-    + hauto lq:on ctrs:rtc use:EReds.BindCong.
-Admitted.

theories/typing.v

@@ -1,251 +0,0 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-
-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_Abs Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  (cons A Γ) ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
-
-| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
-  Γ ⊢ a0 ≡ a1 ∈ A ->
-  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
-
-| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a0 ≡ a1 ∈ A ->
-  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
-  Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
-
-| E_Proj1 Γ (a b : PTm) A B :
-  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
-  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
-
-| 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
-
-(* Eta *)
-| E_AppEta Γ (b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
-
-| E_PairEta Γ (a : PTm ) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
-
-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.
-
-(* Lemma lem : *)
-(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
-(*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
-(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *)
-(*   (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *)
-(* Proof. apply wt_mutual. ... *)