Initial commit

.gitignore

@@ -0,0 +1,63 @@
+.*.aux
+.*.d
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mlg.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+*.vok
+*.vos
+.coq-native
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+native_compute_profile_*.data
+
+# generated timing files
+*.timing.diff
+*.v.after-timing
+*.v.before-timing
+*.v.timing
+time-of-build-after.log
+time-of-build-before.log
+time-of-build-both.log
+time-of-build-pretty.log
+
+# generated coq files
+
+# emacs temporary files
+*~
+
+*.aux
+*.bbl
+*.blg
+*.out
+*.log
+paper/paper-output.tex
+paper/rules.tex
+paper/paper-output.pdf
+proofs
+proofs.zip
+CoqMakefile
+CoqMakefile.conf

Makefile

@@ -0,0 +1,27 @@
+COQMAKEFILE=CoqMakefile
+
+theories: $(COQMAKEFILE) FORCE
+	$(MAKE) -f $(COQMAKEFILE)
+
+validate: $(COQMAKEFILE) FORCE
+	$(MAKE) -f $(COQMAKEFILE) validate
+
+$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v
+	$(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+install: $(COQMAKEFILE)
+	$(MAKE) -f $^ install
+
+uninstall: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE) uninstall
+
+theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
+	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
+
+.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
+
+FORCE:

_CoqProject

@@ -0,0 +1,2 @@
+-R theories ImpredIrrel
+theories

syntax.sig

@@ -0,0 +1,8 @@
+Tm(VarTm) : Type
+-- nat : Type
+
+Abs : (bind Tm in Tm) -> Tm
+App : Tm -> Tm -> Tm
+Pair : Tm -> Tm -> Tm
+Proj1 : Tm -> Tm
+Proj2 : Tm -> Tm

theories/Autosubst2/core.v

@@ -0,0 +1,159 @@
+(* Function composition *)
+
+Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y)  :=
+  fun x => g (f x).
+
+Lemma funcomp_assoc {W X Y Z} (g: Y -> Z) (f: X -> Y) (h: W -> X) :
+  funcomp g (funcomp f h) = (funcomp (funcomp g f) h).
+Proof.
+  reflexivity.
+Qed.
+
+
+(** ** Functor Instances
+
+Exemplary functor instances needed to make Autosubst's generation possible for functors.
+Two things are important:
+1. The names are fixed.
+2. For Coq to check termination, also the proofs have to be closed with Defined.
+ *)
+
+(** *** List Instance *)
+Require Import List.
+
+Notation "'list_map'" := map.
+
+Definition list_ext {A B} {f g : A -> B} :
+  (forall x, f x = g x) -> forall xs, list_map f xs = list_map g xs.
+  intros H. induction xs. reflexivity.
+  cbn. f_equal. apply H. apply IHxs.
+Defined.
+
+Definition list_id {A}  { f : A -> A} :
+  (forall x, f x = x) -> forall xs, list_map f xs = xs.
+Proof.
+  intros H. induction xs. reflexivity.
+  cbn. rewrite H. rewrite IHxs; eauto.
+Defined.
+
+Definition list_comp {A B C} {f: A -> B} {g: B -> C} {h} :
+  (forall x, (funcomp  g f) x = h x) -> forall xs, map g (map f xs) = map h xs.
+Proof.
+  induction xs. reflexivity.
+  cbn. rewrite <- H. f_equal. apply IHxs.
+Defined.
+
+(** *** Prod Instance *)
+
+Definition prod_map {A B C D} (f : A -> C) (g : B -> D) (p : A * B) :
+  C * D.
+Proof.
+  destruct p as [a b]. split.
+  exact (f a). exact (g b).
+Defined.
+
+Definition prod_id {A B} {f : A -> A} {g : B -> B} :
+  (forall x, f x = x) -> (forall x, g x = x) -> forall p, prod_map f g p = p.
+Proof.
+  intros H0 H1. destruct p. cbn. f_equal; [ apply H0 | apply H1 ].
+Defined.
+
+Definition prod_ext {A B C D} {f f' : A -> C} {g g': B -> D} :
+  (forall x, f x = f' x) -> (forall x, g x = g' x) -> forall p, prod_map f g p = prod_map f' g' p.
+Proof.
+  intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ].
+Defined.
+
+Definition prod_comp {A B C D E F} {f1 : A -> C} {g1 : C -> E} {h1 : A -> E} {f2: B -> D} {g2: D -> F} {h2 : B -> F}:
+  (forall x, (funcomp  g1 f1) x = h1 x) -> (forall x, (funcomp g2 f2) x = h2 x) -> forall p, prod_map g1 g2 (prod_map f1 f2 p) = prod_map h1 h2 p.
+Proof.
+  intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ].
+Defined.
+
+(** *** Option Instance *)
+
+Definition option_map {A B} (f : A -> B) (p : option A) :
+  option B :=
+match p with
+  | Some a => Some (f a)
+  | None => None
+end.
+
+Definition option_id {A} {f : A -> A} :
+  (forall x, f x = x) -> forall p, option_map f p = p.
+Proof.
+  intros H. destruct p ; cbn.
+  - f_equal. apply H.
+  - reflexivity.
+Defined.
+
+Definition option_ext {A B} {f f' : A -> B} :
+  (forall x, f x = f' x) -> forall p, option_map f p = option_map f' p.
+Proof.
+  intros H. destruct p as [a|] ; cbn.
+  - f_equal. apply H.
+  - reflexivity.
+Defined.
+
+Definition option_comp {A B C} {f : A -> B} {g : B -> C} {h : A -> C}:
+  (forall x, (funcomp  g f) x = h x) ->
+  forall p, option_map g (option_map f p) = option_map h p.
+Proof.
+  intros H. destruct p as [a|]; cbn.
+  - f_equal. apply H.
+  - reflexivity. 
+Defined.
+
+#[export] Hint Rewrite in_map_iff : FunctorInstances.
+
+(* Declaring the scopes that all our notations will live in *)
+Declare Scope fscope.
+Declare Scope subst_scope.
+
+Ltac eta_reduce :=
+  repeat match goal with
+         | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *)
+         end.
+
+Ltac minimize :=
+  repeat match goal with
+         | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *)
+         | [|- context[fun x => ?g (?f x)]] => change (fun x => g (f x)) with (funcomp g f) (* funcomp folding *)
+         end.
+
+(* had to add this tactic abbreviation because I could not print a setoid_rewrite with the arrow *)
+Ltac setoid_rewrite_left t := setoid_rewrite <- t.
+
+Ltac check_no_evars :=
+  match goal with
+  | [|- ?x] => assert_fails (has_evar x)
+  end.
+
+Require Import Setoid Morphisms.
+
+Lemma pointwise_forall {X Y:Type} (f g: X -> Y) :
+  (pointwise_relation _ eq f g) -> forall x, f x = g x.
+Proof.
+  trivial.
+Qed.
+
+#[export] Instance funcomp_morphism {X Y Z} :
+  Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp.
+Proof.
+  cbv - [funcomp].
+  intros g0 g1 Hg f0 f1 Hf x.
+  unfold funcomp. rewrite Hf, Hg.
+  reflexivity.
+Qed.
+
+#[export] Instance funcomp_morphism2 {X Y Z} :
+  Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> eq ==> eq) funcomp.
+Proof.
+  intros g0 g1 Hg f0 f1 Hf ? x ->.
+  unfold funcomp. rewrite Hf, Hg.
+  reflexivity.
+Qed.
+
+Ltac unfold_funcomp := match goal with
+                           | |-  context[(funcomp ?f ?g) ?s] => change ((funcomp f g) s) with (f (g s))
+                           end.

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

@@ -0,0 +1,774 @@
+Require Import core fintype.
+
+Require Import Setoid Morphisms Relation_Definitions.
+
+
+Module Core.
+
+Inductive Tm (n_Tm : nat) : Type :=
+  | VarTm : fin n_Tm -> Tm n_Tm
+  | Abs : Tm (S n_Tm) -> Tm n_Tm
+  | App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
+  | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
+  | Proj1 : Tm n_Tm -> Tm n_Tm
+  | Proj2 : Tm n_Tm -> Tm n_Tm.
+
+Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
+  (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => Abs m_Tm x) H0)).
+Qed.
+
+Lemma congr_App {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {t0 : Tm m_Tm}
+  {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) :
+  App m_Tm s0 s1 = App m_Tm t0 t1.
+Proof.
+exact (eq_trans (eq_trans eq_refl (ap (fun x => App m_Tm x s1) H0))
+         (ap (fun x => App m_Tm t0 x) H1)).
+Qed.
+
+Lemma congr_Pair {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {t0 : Tm m_Tm}
+  {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) :
+  Pair m_Tm s0 s1 = Pair m_Tm t0 t1.
+Proof.
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair m_Tm x s1) H0))
+         (ap (fun x => Pair m_Tm t0 x) H1)).
+Qed.
+
+Lemma congr_Proj1 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
+  Proj1 m_Tm s0 = Proj1 m_Tm t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => Proj1 m_Tm x) H0)).
+Qed.
+
+Lemma congr_Proj2 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
+  Proj2 m_Tm s0 = Proj2 m_Tm t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => Proj2 m_Tm x) H0)).
+Qed.
+
+Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
+  fin (S m) -> fin (S n).
+Proof.
+exact (up_ren xi).
+Defined.
+
+Lemma upRen_list_Tm_Tm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) :
+  fin (plus p m) -> fin (plus p n).
+Proof.
+exact (upRen_p p xi).
+Defined.
+
+Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
+(s : Tm m_Tm) {struct s} : Tm n_Tm :=
+  match s with
+  | VarTm _ s0 => VarTm n_Tm (xi_Tm s0)
+  | Abs _ s0 => Abs n_Tm (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
+  | App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
+  | Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
+  | Proj1 _ s0 => Proj1 n_Tm (ren_Tm xi_Tm s0)
+  | Proj2 _ s0 => Proj2 n_Tm (ren_Tm xi_Tm s0)
+  end.
+
+Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
+  fin (S m) -> Tm (S n_Tm).
+Proof.
+exact (scons (VarTm (S n_Tm) var_zero) (funcomp (ren_Tm shift) sigma)).
+Defined.
+
+Lemma up_list_Tm_Tm (p : nat) {m : nat} {n_Tm : nat}
+  (sigma : fin m -> Tm n_Tm) : fin (plus p m) -> Tm (plus p n_Tm).
+Proof.
+exact (scons_p p (funcomp (VarTm (plus p n_Tm)) (zero_p p))
+         (funcomp (ren_Tm (shift_p p)) sigma)).
+Defined.
+
+Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
+(s : Tm m_Tm) {struct s} : Tm n_Tm :=
+  match s with
+  | VarTm _ s0 => sigma_Tm s0
+  | Abs _ s0 => Abs n_Tm (subst_Tm (up_Tm_Tm sigma_Tm) s0)
+  | App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
+  | Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
+  | Proj1 _ s0 => Proj1 n_Tm (subst_Tm sigma_Tm s0)
+  | Proj2 _ s0 => Proj2 n_Tm (subst_Tm sigma_Tm s0)
+  end.
+
+Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
+  (Eq : forall x, sigma x = VarTm m_Tm x) :
+  forall x, up_Tm_Tm sigma x = VarTm (S m_Tm) x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n => ap (ren_Tm shift) (Eq fin_n)
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma upId_list_Tm_Tm {p : nat} {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
+  (Eq : forall x, sigma x = VarTm m_Tm x) :
+  forall x, up_list_Tm_Tm p sigma x = VarTm (plus p m_Tm) x.
+Proof.
+exact (fun n =>
+       scons_p_eta (VarTm (plus p m_Tm))
+         (fun n => ap (ren_Tm (shift_p p)) (Eq n)) (fun n => eq_refl)).
+Qed.
+
+Fixpoint idSubst_Tm {m_Tm : nat} (sigma_Tm : fin m_Tm -> Tm m_Tm)
+(Eq_Tm : forall x, sigma_Tm x = VarTm m_Tm x) (s : Tm m_Tm) {struct s} :
+subst_Tm sigma_Tm s = s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
+        (idSubst_Tm sigma_Tm Eq_Tm s1)
+  | Proj1 _ s0 => congr_Proj1 (idSubst_Tm sigma_Tm Eq_Tm s0)
+  | Proj2 _ s0 => congr_Proj2 (idSubst_Tm sigma_Tm Eq_Tm s0)
+  end.
+
+Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
+  (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) :
+  forall x, upRen_Tm_Tm xi x = upRen_Tm_Tm zeta x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n => ap shift (Eq fin_n)
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma upExtRen_list_Tm_Tm {p : nat} {m : nat} {n : nat} (xi : fin m -> fin n)
+  (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) :
+  forall x, upRen_list_Tm_Tm p xi x = upRen_list_Tm_Tm p zeta x.
+Proof.
+exact (fun n =>
+       scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))).
+Qed.
+
+Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
+(zeta_Tm : fin m_Tm -> fin n_Tm) (Eq_Tm : forall x, xi_Tm x = zeta_Tm x)
+(s : Tm m_Tm) {struct s} : ren_Tm xi_Tm s = ren_Tm zeta_Tm s :=
+  match s with
+  | VarTm _ s0 => ap (VarTm n_Tm) (Eq_Tm s0)
+  | Abs _ s0 =>
+      congr_Abs
+        (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
+           (upExtRen_Tm_Tm _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
+  | Proj1 _ s0 => congr_Proj1 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+  | Proj2 _ s0 => congr_Proj2 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+  end.
+
+Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
+  (tau : fin m -> Tm n_Tm) (Eq : forall x, sigma x = tau x) :
+  forall x, up_Tm_Tm sigma x = up_Tm_Tm tau x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n => ap (ren_Tm shift) (Eq fin_n)
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma upExt_list_Tm_Tm {p : nat} {m : nat} {n_Tm : nat}
+  (sigma : fin m -> Tm n_Tm) (tau : fin m -> Tm n_Tm)
+  (Eq : forall x, sigma x = tau x) :
+  forall x, up_list_Tm_Tm p sigma x = up_list_Tm_Tm p tau x.
+Proof.
+exact (fun n =>
+       scons_p_congr (fun n => eq_refl)
+         (fun n => ap (ren_Tm (shift_p p)) (Eq n))).
+Qed.
+
+Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
+(tau_Tm : fin m_Tm -> Tm n_Tm) (Eq_Tm : forall x, sigma_Tm x = tau_Tm x)
+(s : Tm m_Tm) {struct s} : subst_Tm sigma_Tm s = subst_Tm tau_Tm s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs
+        (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
+           s0)
+  | App _ s0 s1 =>
+      congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
+  | Proj1 _ s0 => congr_Proj1 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+  | Proj2 _ s0 => congr_Proj2 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+  end.
+
+Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
+  (zeta : fin l -> fin m) (rho : fin k -> fin m)
+  (Eq : forall x, funcomp zeta xi x = rho x) :
+  forall x, funcomp (upRen_Tm_Tm zeta) (upRen_Tm_Tm xi) x = upRen_Tm_Tm rho x.
+Proof.
+exact (up_ren_ren xi zeta rho Eq).
+Qed.
+
+Lemma up_ren_ren_list_Tm_Tm {p : nat} {k : nat} {l : nat} {m : nat}
+  (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m)
+  (Eq : forall x, funcomp zeta xi x = rho x) :
+  forall x,
+  funcomp (upRen_list_Tm_Tm p zeta) (upRen_list_Tm_Tm p xi) x =
+  upRen_list_Tm_Tm p rho x.
+Proof.
+exact (up_ren_ren_p Eq).
+Qed.
+
+Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+(xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm)
+(rho_Tm : fin m_Tm -> fin l_Tm)
+(Eq_Tm : forall x, funcomp zeta_Tm xi_Tm x = rho_Tm x) (s : Tm m_Tm) {struct
+ s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s :=
+  match s with
+  | VarTm _ s0 => ap (VarTm l_Tm) (Eq_Tm s0)
+  | Abs _ s0 =>
+      congr_Abs
+        (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
+           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
+  | Proj1 _ s0 => congr_Proj1 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+  | Proj2 _ s0 => congr_Proj2 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+  end.
+
+Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
+  (xi : fin k -> fin l) (tau : fin l -> Tm m_Tm) (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp tau xi x = theta x) :
+  forall x, funcomp (up_Tm_Tm tau) (upRen_Tm_Tm xi) x = up_Tm_Tm theta x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n => ap (ren_Tm shift) (Eq fin_n)
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma up_ren_subst_list_Tm_Tm {p : nat} {k : nat} {l : nat} {m_Tm : nat}
+  (xi : fin k -> fin l) (tau : fin l -> Tm m_Tm) (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp tau xi x = theta x) :
+  forall x,
+  funcomp (up_list_Tm_Tm p tau) (upRen_list_Tm_Tm p xi) x =
+  up_list_Tm_Tm p theta x.
+Proof.
+exact (fun n =>
+       eq_trans (scons_p_comp' _ _ _ n)
+         (scons_p_congr (fun z => scons_p_head' _ _ z)
+            (fun z =>
+             eq_trans (scons_p_tail' _ _ (xi z))
+               (ap (ren_Tm (shift_p p)) (Eq z))))).
+Qed.
+
+Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+(xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm)
+(theta_Tm : fin m_Tm -> Tm l_Tm)
+(Eq_Tm : forall x, funcomp tau_Tm xi_Tm x = theta_Tm x) (s : Tm m_Tm) {struct
+ s} : subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs
+        (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
+           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | Proj1 _ s0 =>
+      congr_Proj1 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj2 _ s0 =>
+      congr_Proj2 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+  end.
+
+Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma : fin k -> Tm l_Tm) (zeta_Tm : fin l_Tm -> fin m_Tm)
+  (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) :
+  forall x,
+  funcomp (ren_Tm (upRen_Tm_Tm zeta_Tm)) (up_Tm_Tm sigma) x =
+  up_Tm_Tm theta x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n =>
+           eq_trans
+             (compRenRen_Tm shift (upRen_Tm_Tm zeta_Tm)
+                (funcomp shift zeta_Tm) (fun x => eq_refl) (sigma fin_n))
+             (eq_trans
+                (eq_sym
+                   (compRenRen_Tm zeta_Tm shift (funcomp shift zeta_Tm)
+                      (fun x => eq_refl) (sigma fin_n)))
+                (ap (ren_Tm shift) (Eq fin_n)))
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma up_subst_ren_list_Tm_Tm {p : nat} {k : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma : fin k -> Tm l_Tm) (zeta_Tm : fin l_Tm -> fin m_Tm)
+  (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) :
+  forall x,
+  funcomp (ren_Tm (upRen_list_Tm_Tm p zeta_Tm)) (up_list_Tm_Tm p sigma) x =
+  up_list_Tm_Tm p theta x.
+Proof.
+exact (fun n =>
+       eq_trans (scons_p_comp' _ _ _ n)
+         (scons_p_congr
+            (fun x => ap (VarTm (plus p m_Tm)) (scons_p_head' _ _ x))
+            (fun n =>
+             eq_trans
+               (compRenRen_Tm (shift_p p) (upRen_list_Tm_Tm p zeta_Tm)
+                  (funcomp (shift_p p) zeta_Tm)
+                  (fun x => scons_p_tail' _ _ x) (sigma n))
+               (eq_trans
+                  (eq_sym
+                     (compRenRen_Tm zeta_Tm (shift_p p)
+                        (funcomp (shift_p p) zeta_Tm) (fun x => eq_refl)
+                        (sigma n))) (ap (ren_Tm (shift_p p)) (Eq n)))))).
+Qed.
+
+Fixpoint compSubstRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+(sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm)
+(theta_Tm : fin m_Tm -> Tm l_Tm)
+(Eq_Tm : forall x, funcomp (ren_Tm zeta_Tm) sigma_Tm x = theta_Tm x)
+(s : Tm m_Tm) {struct s} :
+ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs
+        (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
+           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
+  | Proj1 _ s0 =>
+      congr_Proj1 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+  | Proj2 _ s0 =>
+      congr_Proj2 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+  end.
+
+Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma : fin k -> Tm l_Tm) (tau_Tm : fin l_Tm -> Tm m_Tm)
+  (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) :
+  forall x,
+  funcomp (subst_Tm (up_Tm_Tm tau_Tm)) (up_Tm_Tm sigma) x = up_Tm_Tm theta x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n =>
+           eq_trans
+             (compRenSubst_Tm shift (up_Tm_Tm tau_Tm)
+                (funcomp (up_Tm_Tm tau_Tm) shift) (fun x => eq_refl)
+                (sigma fin_n))
+             (eq_trans
+                (eq_sym
+                   (compSubstRen_Tm tau_Tm shift
+                      (funcomp (ren_Tm shift) tau_Tm) (fun x => eq_refl)
+                      (sigma fin_n))) (ap (ren_Tm shift) (Eq fin_n)))
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma up_subst_subst_list_Tm_Tm {p : nat} {k : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma : fin k -> Tm l_Tm) (tau_Tm : fin l_Tm -> Tm m_Tm)
+  (theta : fin k -> Tm m_Tm)
+  (Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) :
+  forall x,
+  funcomp (subst_Tm (up_list_Tm_Tm p tau_Tm)) (up_list_Tm_Tm p sigma) x =
+  up_list_Tm_Tm p theta x.
+Proof.
+exact (fun n =>
+       eq_trans
+         (scons_p_comp' (funcomp (VarTm (plus p l_Tm)) (zero_p p)) _ _ n)
+         (scons_p_congr
+            (fun x => scons_p_head' _ (fun z => ren_Tm (shift_p p) _) x)
+            (fun n =>
+             eq_trans
+               (compRenSubst_Tm (shift_p p) (up_list_Tm_Tm p tau_Tm)
+                  (funcomp (up_list_Tm_Tm p tau_Tm) (shift_p p))
+                  (fun x => eq_refl) (sigma n))
+               (eq_trans
+                  (eq_sym
+                     (compSubstRen_Tm tau_Tm (shift_p p) _
+                        (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n)))
+                  (ap (ren_Tm (shift_p p)) (Eq n)))))).
+Qed.
+
+Fixpoint compSubstSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+(sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm)
+(theta_Tm : fin m_Tm -> Tm l_Tm)
+(Eq_Tm : forall x, funcomp (subst_Tm tau_Tm) sigma_Tm x = theta_Tm x)
+(s : Tm m_Tm) {struct s} :
+subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs
+        (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
+           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | Proj1 _ s0 =>
+      congr_Proj1 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj2 _ s0 =>
+      congr_Proj2 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+  end.
+
+Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm)
+  (s : Tm m_Tm) :
+  ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm (funcomp zeta_Tm xi_Tm) s.
+Proof.
+exact (compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma renRen'_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) :
+  pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (ren_Tm xi_Tm))
+    (ren_Tm (funcomp zeta_Tm xi_Tm)).
+Proof.
+exact (fun s => compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma renSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) (s : Tm m_Tm)
+  : subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm (funcomp tau_Tm xi_Tm) s.
+Proof.
+exact (compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma renSubst_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) :
+  pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (ren_Tm xi_Tm))
+    (subst_Tm (funcomp tau_Tm xi_Tm)).
+Proof.
+exact (fun s => compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma substRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm)
+  (s : Tm m_Tm) :
+  ren_Tm zeta_Tm (subst_Tm sigma_Tm s) =
+  subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm) s.
+Proof.
+exact (compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma substRen_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) :
+  pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (subst_Tm sigma_Tm))
+    (subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm)).
+Proof.
+exact (fun s => compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma substSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm)
+  (s : Tm m_Tm) :
+  subst_Tm tau_Tm (subst_Tm sigma_Tm s) =
+  subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm) s.
+Proof.
+exact (compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma substSubst_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
+  (sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) :
+  pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (subst_Tm sigma_Tm))
+    (subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm)).
+Proof.
+exact (fun s => compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma rinstInst_up_Tm_Tm {m : nat} {n_Tm : nat} (xi : fin m -> fin n_Tm)
+  (sigma : fin m -> Tm n_Tm)
+  (Eq : forall x, funcomp (VarTm n_Tm) xi x = sigma x) :
+  forall x, funcomp (VarTm (S n_Tm)) (upRen_Tm_Tm xi) x = up_Tm_Tm sigma x.
+Proof.
+exact (fun n =>
+       match n with
+       | Some fin_n => ap (ren_Tm shift) (Eq fin_n)
+       | None => eq_refl
+       end).
+Qed.
+
+Lemma rinstInst_up_list_Tm_Tm {p : nat} {m : nat} {n_Tm : nat}
+  (xi : fin m -> fin n_Tm) (sigma : fin m -> Tm n_Tm)
+  (Eq : forall x, funcomp (VarTm n_Tm) xi x = sigma x) :
+  forall x,
+  funcomp (VarTm (plus p n_Tm)) (upRen_list_Tm_Tm p xi) x =
+  up_list_Tm_Tm p sigma x.
+Proof.
+exact (fun n =>
+       eq_trans (scons_p_comp' _ _ (VarTm (plus p n_Tm)) n)
+         (scons_p_congr (fun z => eq_refl)
+            (fun n => ap (ren_Tm (shift_p p)) (Eq n)))).
+Qed.
+
+Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
+(xi_Tm : fin m_Tm -> fin n_Tm) (sigma_Tm : fin m_Tm -> Tm n_Tm)
+(Eq_Tm : forall x, funcomp (VarTm n_Tm) xi_Tm x = sigma_Tm x) (s : Tm m_Tm)
+{struct s} : ren_Tm xi_Tm s = subst_Tm sigma_Tm s :=
+  match s with
+  | VarTm _ s0 => Eq_Tm s0
+  | Abs _ s0 =>
+      congr_Abs
+        (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
+           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0)
+  | App _ s0 s1 =>
+      congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
+  | Pair _ s0 s1 =>
+      congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
+  | Proj1 _ s0 => congr_Proj1 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+  | Proj2 _ s0 => congr_Proj2 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+  end.
+
+Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
+  (s : Tm m_Tm) : ren_Tm xi_Tm s = subst_Tm (funcomp (VarTm n_Tm) xi_Tm) s.
+Proof.
+exact (rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma rinstInst'_Tm_pointwise {m_Tm : nat} {n_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin n_Tm) :
+  pointwise_relation _ eq (ren_Tm xi_Tm)
+    (subst_Tm (funcomp (VarTm n_Tm) xi_Tm)).
+Proof.
+exact (fun s => rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
+Qed.
+
+Lemma instId'_Tm {m_Tm : nat} (s : Tm m_Tm) : subst_Tm (VarTm m_Tm) s = s.
+Proof.
+exact (idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s).
+Qed.
+
+Lemma instId'_Tm_pointwise {m_Tm : nat} :
+  pointwise_relation _ eq (subst_Tm (VarTm m_Tm)) id.
+Proof.
+exact (fun s => idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s).
+Qed.
+
+Lemma rinstId'_Tm {m_Tm : nat} (s : Tm m_Tm) : ren_Tm id s = s.
+Proof.
+exact (eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
+Qed.
+
+Lemma rinstId'_Tm_pointwise {m_Tm : nat} :
+  pointwise_relation _ eq (@ren_Tm m_Tm m_Tm id) id.
+Proof.
+exact (fun s => eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
+Qed.
+
+Lemma varL'_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
+  (x : fin m_Tm) : subst_Tm sigma_Tm (VarTm m_Tm x) = sigma_Tm x.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma varL'_Tm_pointwise {m_Tm : nat} {n_Tm : nat}
+  (sigma_Tm : fin m_Tm -> Tm n_Tm) :
+  pointwise_relation _ eq (funcomp (subst_Tm sigma_Tm) (VarTm m_Tm)) sigma_Tm.
+Proof.
+exact (fun x => eq_refl).
+Qed.
+
+Lemma varLRen'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
+  (x : fin m_Tm) : ren_Tm xi_Tm (VarTm m_Tm x) = VarTm n_Tm (xi_Tm x).
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma varLRen'_Tm_pointwise {m_Tm : nat} {n_Tm : nat}
+  (xi_Tm : fin m_Tm -> fin n_Tm) :
+  pointwise_relation _ eq (funcomp (ren_Tm xi_Tm) (VarTm m_Tm))
+    (funcomp (VarTm n_Tm) xi_Tm).
+Proof.
+exact (fun x => eq_refl).
+Qed.
+
+Class Up_Tm X Y :=
+    up_Tm : X -> Y.
+
+#[global]
+Instance Subst_Tm  {m_Tm n_Tm : nat}: (Subst1 _ _ _) := (@subst_Tm m_Tm n_Tm).
+
+#[global]
+Instance Up_Tm_Tm  {m n_Tm : nat}: (Up_Tm _ _) := (@up_Tm_Tm m n_Tm).
+
+#[global]
+Instance Ren_Tm  {m_Tm n_Tm : nat}: (Ren1 _ _ _) := (@ren_Tm m_Tm n_Tm).
+
+#[global]
+Instance VarInstance_Tm  {n_Tm : nat}: (Var _ _) := (@VarTm n_Tm).
+
+Notation "[ sigma_Tm ]" := (subst_Tm sigma_Tm)
+( at level 1, left associativity, only printing)  : fscope.
+
+Notation "s [ sigma_Tm ]" := (subst_Tm sigma_Tm s)
+( at level 7, left associativity, only printing)  : subst_scope.
+
+Notation "↑__Tm" := up_Tm (only printing)  : subst_scope.
+
+Notation "↑__Tm" := up_Tm_Tm (only printing)  : subst_scope.
+
+Notation "⟨ xi_Tm ⟩" := (ren_Tm xi_Tm)
+( at level 1, left associativity, only printing)  : fscope.
+
+Notation "s ⟨ xi_Tm ⟩" := (ren_Tm xi_Tm s)
+( at level 7, left associativity, only printing)  : subst_scope.
+
+Notation "'var'" := VarTm ( at level 1, only printing)  : subst_scope.
+
+Notation "x '__Tm'" := (@ids _ _ VarInstance_Tm x)
+( at level 5, format "x __Tm", only printing)  : subst_scope.
+
+Notation "x '__Tm'" := (VarTm x) ( at level 5, format "x __Tm")  :
+subst_scope.
+
+#[global]
+Instance subst_Tm_morphism  {m_Tm : nat} {n_Tm : nat}:
+ (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
+    (@subst_Tm m_Tm n_Tm)).
+Proof.
+exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
+       eq_ind s (fun t' => subst_Tm f_Tm s = subst_Tm g_Tm t')
+         (ext_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
+Qed.
+
+#[global]
+Instance subst_Tm_morphism2  {m_Tm : nat} {n_Tm : nat}:
+ (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
+    (@subst_Tm m_Tm n_Tm)).
+Proof.
+exact (fun f_Tm g_Tm Eq_Tm s => ext_Tm f_Tm g_Tm Eq_Tm s).
+Qed.
+
+#[global]
+Instance ren_Tm_morphism  {m_Tm : nat} {n_Tm : nat}:
+ (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
+    (@ren_Tm m_Tm n_Tm)).
+Proof.
+exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
+       eq_ind s (fun t' => ren_Tm f_Tm s = ren_Tm g_Tm t')
+         (extRen_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
+Qed.
+
+#[global]
+Instance ren_Tm_morphism2  {m_Tm : nat} {n_Tm : nat}:
+ (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
+    (@ren_Tm m_Tm n_Tm)).
+Proof.
+exact (fun f_Tm g_Tm Eq_Tm s => extRen_Tm f_Tm g_Tm Eq_Tm s).
+Qed.
+
+Ltac auto_unfold := repeat
+                     unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1,
+                      Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1.
+
+Tactic Notation "auto_unfold" "in" "*" := repeat
+                                           unfold VarInstance_Tm, Var, ids,
+                                            Ren_Tm, Ren1, ren1, Up_Tm_Tm,
+                                            Up_Tm, up_Tm, Subst_Tm, Subst1,
+                                            subst1 in *.
+
+Ltac asimpl' := repeat (first
+                 [ progress setoid_rewrite substSubst_Tm_pointwise
+                 | progress setoid_rewrite substSubst_Tm
+                 | progress setoid_rewrite substRen_Tm_pointwise
+                 | progress setoid_rewrite substRen_Tm
+                 | progress setoid_rewrite renSubst_Tm_pointwise
+                 | progress setoid_rewrite renSubst_Tm
+                 | progress setoid_rewrite renRen'_Tm_pointwise
+                 | progress setoid_rewrite renRen_Tm
+                 | progress setoid_rewrite varLRen'_Tm_pointwise
+                 | progress setoid_rewrite varLRen'_Tm
+                 | progress setoid_rewrite varL'_Tm_pointwise
+                 | progress setoid_rewrite varL'_Tm
+                 | progress setoid_rewrite rinstId'_Tm_pointwise
+                 | progress setoid_rewrite rinstId'_Tm
+                 | progress setoid_rewrite instId'_Tm_pointwise
+                 | progress setoid_rewrite instId'_Tm
+                 | progress
+                    unfold up_list_Tm_Tm, up_Tm_Tm, upRen_list_Tm_Tm,
+                     upRen_Tm_Tm, up_ren
+                 | progress cbn[subst_Tm ren_Tm]
+                 | progress fsimpl ]).
+
+Ltac asimpl := check_no_evars;
+                repeat
+                 unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1,
+                  Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1 in *;
+                asimpl'; minimize.
+
+Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
+
+Tactic Notation "auto_case" := auto_case ltac:(asimpl; cbn; eauto).
+
+Ltac substify := auto_unfold; try setoid_rewrite rinstInst'_Tm_pointwise;
+                  try setoid_rewrite rinstInst'_Tm.
+
+Ltac renamify := auto_unfold; try setoid_rewrite_left rinstInst'_Tm_pointwise;
+                  try setoid_rewrite_left rinstInst'_Tm.
+
+End Core.
+
+Module Extra.
+
+Import
+Core.
+
+Arguments VarTm {n_Tm}.
+
+Arguments Proj2 {n_Tm}.
+
+Arguments Proj1 {n_Tm}.
+
+Arguments Pair {n_Tm}.
+
+Arguments App {n_Tm}.
+
+Arguments Abs {n_Tm}.
+
+#[global]Hint Opaque subst_Tm: rewrite.
+
+#[global]Hint Opaque ren_Tm: rewrite.
+
+End Extra.
+
+Module interface.
+
+Export Core.
+
+Export Extra.
+
+End interface.
+
+Export interface.
+