# System F + constants Terms

This file contains the definition of System F Terms with a constant and their multivariate traversals and models. This is needed for the proof of strong normalisation. The definitions are not contained explicitly, but we refer to the corrresponding lemmas for FCBV in Chapter 5.
This part of the code is intended to be generated by Autosubst 2.
From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Framework.graded Framework.sysf_types.
Set Implicit Arguments.
Unset Strict Implicit.

Local Ltac asimpl :=
repeat progress (cbn; fsimpl; gsimpl; ty_simpl).

Module TmVl.
Section Defs.
Inductive tm (m n : nat) :=
| var (x : fin n)
| lam (A : ty m) (b : tm m n.+1)
| Lam (b : tm m.+1 n)
| app (s : tm m n) (t : tm m n)
| App (s : tm m n) (A : ty m)
| const.
Arguments var {m n}, m n.

## Traversals and their Evaluation

The type traversal Vty Dty Vtm Dtm represents a traversal (cf. Definition 5.1) parameterised by semantic value domains Vty and Vtm and semantic expression domains Dty and Dtm.
Evaluation (cf. Definition 5.3) requires the corresponding semantic value domains to be graded, respectively bigraded (cf. Definition 3.2, Definition 5.2).

Structure traversal (Vty Dty : nat -> Type) (Vtm Dtm : nat -> nat -> Type) := Traversal
{ tvar : forall m n, Vtm m n -> Dtm m n
; tlam : forall m n, Dty m -> (fun m n => Vtm m n -> Dtm m n) m n -> Dtm m n
; tLam : forall m n, (fun m n => Vty m -> Dtm m n) m n -> Dtm m n
; tapp : forall m n, Dtm m n -> Dtm m n -> Dtm m n
; tApp : forall m n, Dtm m n -> Dty m -> Dtm m n
; tconst : forall m n, Dtm m n
}.
Arguments tvar {Vty Dty Vtm Dtm} t {m n} i.
Arguments tlam {Vty Dty Vtm Dtm} t {m n} A F.
Arguments tLam {Vty Dty Vtm Dtm} t {m n} F.
Arguments tapp {Vty Dty Vtm Dtm} t {m n} f a.
Arguments tApp {Vty Dty Vtm Dtm} t {m n} f A.
Arguments tconst {Vty Dty Vtm Dtm} t {m n}.

Fixpoint eval {Vty : graded1} {Dty : nat -> Type} {Vtm : graded2} {Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vtm Dtm)
{m1 n1 m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vtm m2 n2) (v : tm m1 n1) : Dtm m2 n2 :=
match v with
| var i => tvar E (theta i)
| lam A b => tlam E (Ty.eval T rho A) (fun _ _ f g v => eval T E (rho >> th1 f) (v .: theta >> th2 f g) b)
| Lam b => tLam E (fun _ _ f g v => eval T E (v .: rho >> th1 f) (theta >> th2 f g) b)
| app s t => tapp E (eval T E rho theta s) (eval T E rho theta t)
| App s A => tApp E (eval T E rho theta s) (Ty.eval T rho A)
| const => tconst E
end.

## Models (cf. Definition 5.4)

A traversal is a model if it satisfies additional naturality conditions.

Structure is_natural {Vty Dty : graded1} {Vtm Dtm : graded2} (E : traversal Vty Dty Vtm Dtm) := IsNatural
{ nvar : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (i : Vtm m1 n1),
(tvar E i) (xi,zeta) = tvar E (i (xi,zeta))
; nlam : forall m1 n1 (A : Dty m1) (F : (fun m n => Vtm m n -> Dtm m n) m1 n1),
(forall m2 m3 n2 n3 (xi1 : iren m1 m2) (xi2 : iren m2 m3) (zeta1 : iren n1 n2) (zeta2 : iren n2 n3) (i : Vtm m2 n2),
(F m2 n2 xi1 zeta1 i) (xi2,zeta2) = F m3 n3 (xi1 >>> xi2) (zeta1 >>> zeta2) (i (xi2,zeta2))) ->
forall m2 n2 (xi : iren m1 m2) (zeta : iren n1 n2),
(tlam E A F) (xi,zeta) = tlam E (A xi) (F (xi,zeta))
; nLam : forall m1 n1 (F : (fun m n => Vty m -> Dtm m n) m1 n1),
(forall m2 m3 n2 n3 (xi1 : iren m1 m2) (xi2 : iren m2 m3) (zeta1 : iren n1 n2) (zeta2 : iren n2 n3) (i : Vty m2),
(F m2 n2 xi1 zeta1 i) (xi2,zeta2) = F m3 n3 (xi1 >>> xi2) (zeta1 >>> zeta2) (i xi2)) ->
forall m2 n2 (xi : iren m1 m2) (zeta : iren n1 n2),
(tLam E F) (xi,zeta) = tLam E (F (xi,zeta))
; napp : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (a b : Dtm m1 n1),
(tapp E a b) (xi,zeta) = tapp E (a (xi,zeta)) (b (xi,zeta))
; nApp : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (a : Dtm m1 n1) (A : Dty m1),
(tApp E a A) (xi,zeta) = tApp E (a (xi,zeta)) (A xi)
; nconst : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2),
(tconst E) (xi,zeta) = tconst E
}.

Structure model (Vty Dty : graded1) (Vtm Dtm : graded2) := Model
{ base : traversal Vty Dty Vtm Dtm
; _ : is_natural base
}.
Local Coercion base : model >-> traversal.

Definition model_is_natural {Vty Dty : graded1} {Vtm Dtm : graded2} (t : model Vty Dty Vtm Dtm) : is_natural t :=
let: Model _ c := t in c.
Local Coercion model_is_natural : model >-> is_natural.

## Renaming (cf. Definition 5.6)

Definition and properties.

Definition ren_traversal : traversal fin ty fin2 tm :=
Traversal (@var) (fun m n A F => lam A (F m n.+1 idren shift bound))
(fun m n F => Lam (F m.+1 n shift idren bound))
(@app) (@App) (@const).
Local Notation tm_ren := (eval Ty.ren_traversal ren_traversal).
Canonical tm_graded2 := Eval hnf in Graded2 tm (@eval _ _ _ _ Ty.ren_traversal ren_traversal).

Lemma th2_tmE {m1 m2 n1 n2} (xi : iren m1 m2) (zeta : iren n1 n2) (s : tm m1 n1) :
s (xi, zeta) = tm_ren xi zeta s.
Proof. by []. Qed.

Lemma ren_is_natural : is_natural ren_traversal.
Proof.
apply: IsNatural => //=[m1 n1 A|m1 n1] F H m2 n2 xi zeta.
- rewrite th2_tmE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ _ _ (up zeta)).
- rewrite th2_tmE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ (up xi)).
Qed.
Canonical ren_model := Eval hnf in Model ren_is_natural.

Lemma ren_tm_id m n (s : tm m n) :
tm_ren id id s = s.
Proof.
elim: s => {m n}//=[m n A b ih|m n b ih|m n s->t->|m n s->A]//.
- asimpl. by rewrite ih.
- asimpl. by rewrite ih.
- by asimpl.
Qed.

Section EvalRen.
Context {Vty : graded1} {Dty : nat -> Type} {Vtm : graded2} {Dtm : nat -> nat -> Type}
(T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vtm Dtm).

cf. Theorem 5.7
Lemma eval_ren m1 m2 m3 n1 n2 n3 (xi : ren m1 m2) (zeta : ren n1 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vtm m3 n3) (s : tm m1 n1) :
eval T E rho theta (tm_ren xi zeta s) = eval T E (xi >> rho) (zeta >> theta) s.
Proof.
elim: s m2 m3 n2 n3 xi zeta rho theta => {m1 n1}//=[m n A b ih|m n b ih|m n s ihs t iht|m n s ih A] m2 m3 n2 n3 xi zeta rho theta.
- asimpl. f_equal;fext=> m4 n4 f' g' i. rewrite ih. by asimpl.
- f_equal;fext=> m4 n4 f' g' i. rewrite ih. by asimpl.
- by rewrite ihs iht.
- asimpl. by rewrite ih.
Qed.
End EvalRen.

Lemma ren_comp {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (xi2 : ren m2 m3)
(zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (s : tm m1 n1) :
tm_ren xi2 zeta2 (tm_ren xi1 zeta1 s) = tm_ren (xi1 >> xi2) (zeta1 >> zeta2) s.
Proof. exact: eval_ren. Qed.

Lemma ren_tm_inj m1 m2 n1 n2 (xi : ren m1 m2) (zeta : ren n1 n2) (s1 s2 : tm m1 n1) :
injective xi -> injective zeta -> tm_ren xi zeta s1 = tm_ren xi zeta s2 -> s1 = s2.
Proof.
elim: s1 s2 m2 n2 xi zeta => {m1 n1}[m1 n1 i|m1 n1 A1 b1 ih|m1 n1 b1 ih|m1 n1 s1 ihs t1 iht|m1 n1 s1 ih A1|m1 n1].
- by move=> [j|||||]//= m2 n2 xi zeta fP gP [/gP->].
- move=> [|A2 b2||||]//= m2 n2 xi zeta fP gP [/(Ty.ren_inj fP)->/ih->//].
by move=> /=[i|] [j|]//=[/gP->].
- by move=> [||b2|||]//= m2 n2 xi zeta fP gP [/ih->//] /=[i|] [j|]//=[/fP->].
- by move=> [|||s2 t2||]//= m2 n2 xi zeta fP gP [/ihs->///iht->].
- by move=> [||||s2 A2|]//= m2 n2 xi zeta fP gP [/ih->///Ty.ren_inj->].
- by case.
Qed.
Canonical tm_pgraded2 := Eval hnf in PGraded2 tm (fun m1 m2 n1 n2 xi zeta v1 v2 =>
@ren_tm_inj m1 m2 n1 n2 xi zeta v1 v2 (@iren_inj _ _ xi) (@iren_inj _ _ zeta)).

## Lifting (cf. Definition 5.5)

Definition lift {Vty Dty : nat -> Type} {Vtm Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vtm Dtm) : traversal Dty Dty Dtm Dtm.
apply: Traversal.
- exact (fun _ _ => id).
- intros m n A F. apply (tlam E). exact A. intros m' n' xi zeta v. apply (F m' n' xi zeta).
apply (tvar E). exact v.
- intros m n F. apply (tLam E). intros m' n' xi zeta v. apply (F m' n' xi zeta).
apply (Ty.tvar T). exact v.
- exact (@tapp _ _ _ _ E).
- exact (@tApp _ _ _ _ E).
- exact (@tconst _ _ _ _ E).
Defined.

Definition lift_is_natural {Vty Dty : graded1} {Vtm Dtm : graded2} (T : Ty.model Vty Dty)
(E : model Vty Dty Vtm Dtm) :
is_natural (lift T E).
Proof.
apply: IsNatural => //=[m1 n1 A F H m2 n2 xi g|m1 n1 F H m2 n2 xi g|m1 m2 n1 n2 xi zeta a b|m1 m2 n1 n2 xi zeta a A|m1 n1].
- apply: (nlam E); intros; by rewrite H (nvar E).
- apply: (nLam E); intros; by rewrite H (Ty.nvar T).
- exact: (napp E).
- exact: (nApp E).
- exact: (nconst E).
Qed.

Canonical lift_model {Vty Dty : graded1} {Vtm Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vtm Dtm) : model Dty Dty Dtm Dtm :=
Eval hnf in Model (lift_is_natural T E).

## Theorem 5.8

Lemma lift_embed {Vty Dty : graded1} {Vtm Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vtm Dtm) {m1 m2 n1 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vtm m2 n2) (s : tm m1 n1) :
eval T E rho theta s = eval (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) s.
Proof.
elim: s m2 n2 rho theta =>{m1 n1}//=[m1 n1 A b ih|m1 n1 b ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 n2 rho theta.
- rewrite Ty.embed. f_equal;fext=> m3 n3 xi zeta i. rewrite ih. asimpl. f_equal; fext=> j /=. symmetry. exact: (Ty.nvar T). case: j => //= j. symmetry. exact: (nvar E).
- f_equal;fext=> m3 n3 xi zeta i. rewrite ih. asimpl. f_equal;fext=>/=. case=> //= j. symmetry.
exact: (Ty.nvar T). move=> j /=. symmetry. exact: (nvar E).
- by rewrite ihs iht.
- by rewrite ihs Ty.embed.
Qed.

## Instantiation

Notation inst_traversal := (lift Ty.ren_traversal ren_traversal).
Notation inst_tm := (eval Ty.inst_traversal inst_traversal).
Notation "s .[ sigma , tau ]" := (inst_tm sigma tau s)
(at level 2, left associativity, format "s .[ sigma , tau ]") : tm_inst_scope.
Delimit Scope tm_inst_scope with tm.

Definition inst_tm_id {m n : nat} (s : tm m n) :
s.[Ty.var, var]%tm = s.
Proof.
rewrite -{2}[s]th_id2/=. symmetry. exact: lift_embed.
Qed.

Definition tm_ren_inst {m1 m2 m3 n1 n2 n3 : nat} (xi : ren m1 m2) (zeta : ren n1 n2) (sigma : fin m2 -> ty m3) (tau : fin n2 -> tm m3 n3) (s : tm m1 n1) :
(tm_ren xi zeta s).[sigma, tau]%tm = s.[xi >> sigma, zeta >> tau]%tm.
Proof. exact: eval_ren. Qed.

## Naturality

Lemma naturality {Vty : cgraded1} {Dty : graded1} {Vtm : cgraded2} {Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vtm Dtm) {m1 m2 m3 n1 n2 n3 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vtm m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3) (s : tm m1 n1) :
(eval T E rho theta s) (xi,zeta) = eval T E (rho >> th1 xi) (theta >> th2 xi zeta) s.
Proof.
elim: s m2 m3 n2 n3 rho theta xi zeta =>{m1 n1}[m1 n1 i|m1 n1 A b ih|m1 n1 b ih|m1 n1 s ihs t iht|m1 n1 s ihs A|m1 n1] m2 m3 n2 n3 rho theta xi zeta.
- exact: (nvar E).
- cbn. rewrite (nlam E). f_equal. by asimpl. fext=> m4 n4 xi' zeta' i /=. by asimpl.
intros. rewrite ih. by asimpl.
- cbn. rewrite (nLam E). f_equal. fext=> /=m4 n4 xi' zeta' i. by asimpl.
intros. rewrite ih. by asimpl.
- by rewrite/=(napp E) ihs iht.
- by rewrite/=(nApp E) ihs Ty.naturality.
- exact: (nconst E).
Qed.

## Compatibility with instantiation

Shown via the definition of models.
Theorem 5.9
(T : Ty.model Vty Dty) (E : model Vty Dty Vtm Dtm) (m1 n1 : nat) :
(forall (s : tm m1 n1) {m2 m3 n2 n3 : nat} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2)
(rho : fin m2 -> Vty m3) (theta : fin n2 -> Vtm m3 n3),
eval T E rho theta s.[sigma, tau]%tm =
eval (Ty.lift T) (lift T E) (sigma >> Ty.eval T rho) (tau >> eval T E rho theta) s).
Proof.
elim=>{m1 n1}//=[m1 n1 A b ih|m1 n1 b ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 m3 n2 n3 sigma tau rho theta.
- f_equal. by asimpl. fext=>/=m4 n4 sigma' tau' i. rewrite ih. f_equal.
fext=>j/=. by asimpl.
fext=>/=-[]//=j. rewrite eval_ren. symmetry. exact: naturality.
- f_equal;fext=>/=m4 n4 sigma' tau' i. rewrite ih /=. f_equal.
fext=>/=-[]//=j. by asimpl.
fext=>/=j. rewrite eval_ren. symmetry. exact: naturality.
- by rewrite ihs iht.
- asimpl. by rewrite ihs.
Qed.

Lemma inst_comp {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> tm m2 n2)
(sigma2 : fin m2 -> ty m3) (tau2 : fin n2 -> tm m3 n3) (s : tm m1 n1) :
s.[sigma1,tau1]%tm.[sigma2,tau2]%tm = s.[sigma1 >> Ty.inst sigma2, tau1 >> inst_tm sigma2 tau2]%tm.
Proof. exact: eval_inst. Qed.

Lemma tm_inst_ren {m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) (xi : ren m2 m3) (zeta : ren n2 n3) (s : tm m1 n1) :
tm_ren xi zeta s.[sigma,tau]%tm = s.[sigma >> Ty.ren xi, tau>> tm_ren xi zeta]%tm.
Proof.
rewrite lift_embed inst_comp. f_equal; fext => i /=; symmetry.
exact: Ty.embed. exact: lift_embed.
Qed.

End Defs.

## Exports

Exports the definitions later visible for the user.

Module Exports.
Notation tm := tm.

Canonical ren_model.
Canonical lift_model.

Coercion base : model >-> traversal.
Coercion model_is_natural : model >-> is_natural.

Arguments var {m n}, m n.

Arguments tvar {Vty Dty Vtm Dtm} t {m n} i.
Arguments tlam {Vty Dty Vtm Dtm} t {m n} A F.
Arguments tLam {Vty Dty Vtm Dtm} t {m n} F.
Arguments tapp {Vty Dty Vtm Dtm} t {m n} xi a.
Arguments tApp {Vty Dty Vtm Dtm} t {m n} xi A.
Arguments tconst {Vty Dty Vtm Dtm} t {m n}.

Module Tm.
Notation traversal := traversal.
Notation Traversal := Traversal.
Notation tvar := tvar.
Notation tlam := tlam.
Notation tLam := tLam.
Notation tapp := tapp.
Notation tApp := tApp.
Notation tconst := tconst.

Notation ren_traversal := ren_traversal.
Notation inst_traversal := (lift Ty.ren_traversal ren_traversal).
Notation lift := lift.

Notation is_natural := is_natural.
Notation IsNatural := IsNatural.
Notation nvar := nvar.
Notation nlam := nlam.
Notation nLam := nLam.
Notation napp := napp.
Notation nApp := nApp.
Notation nconst := nconst.

Notation model := model.
Notation Model := Model.

(* Types *)
Notation var := var.
Notation lam := lam.
Notation Lam := Lam.
Notation app := app.
Notation App := App.
Notation const := const.

(* Evaluation *)
Notation eval := eval.

Notation eval_ren := eval_ren.
Notation eval_inst := eval_inst.
Notation naturality := naturality.

Notation embed := lift_embed.

(* Renaming *)
Notation ren := (eval Ty.ren_traversal ren_traversal).

Notation ren_id := ren_tm_id.
Notation ren_comp := ren_comp.
Notation ren_inj := ren_tm_inj.

(* Instantiation *)
Notation inst := (eval Ty.inst_traversal inst_traversal).

Notation ren_inst := tm_ren_inst.
Notation inst_ren := tm_inst_ren.

Notation inst_id := inst_tm_id.
Notation inst_comp := inst_comp.
End Tm.

Notation "s ◁ ( xi , zeta )" := (Tm.ren xi zeta s) (at level 50,
format "s ◁ ( xi , zeta )") : tm_inst_scope.

Notation "s .[ sigma , tau ]" := (Tm.inst sigma tau s)
(at level 2, left associativity, format "s .[ sigma , tau ]") : tm_inst_scope.

Delimit Scope tm_inst_scope with tm.
End Exports.
End TmVl.
Export TmVl.Exports.

## Automation

Lemmas needed for the automation for terms. The statements are chosen according to the lemmas of Autosubst 2 and repeatedly rewritten. See the LFMTP progress paper for more details.
Lemma tm_ren_idX {m n} : Tm.ren (id : fin m -> fin m) (id : fin n -> fin n) = id.
Proof. fext=> A. exact: Tm.ren_id. Qed.

Lemma tm_ren_compX {m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) :
Tm.ren xi1 zeta1 >> Tm.ren xi2 zeta2 = Tm.ren (xi1 >> xi2) (zeta1 >> zeta2).
Proof. fext=> A /=. exact: Tm.ren_comp. Qed.

Lemma tm_ren_compR {T m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (h : _ -> T) :
Tm.ren xi1 zeta1 >> (Tm.ren xi2 zeta2 >> h) = Tm.ren (xi1 >> xi2) (zeta1 >> zeta2) >> h.
Proof. fext=> A /=. by rewrite Tm.ren_comp. Qed.

Lemma tm_ren_instX {m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> tm m3 n3) :
Tm.ren xi zeta >> Tm.inst sigma tau = Tm.inst (xi >> sigma) (zeta >> tau).
Proof. fext=> A /=. exact: Tm.ren_inst. Qed.

Lemma tm_ren_instR {T m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> tm m3 n3) (h : _ -> T) :
Tm.ren xi zeta >> (Tm.inst sigma tau >> h) = Tm.inst (xi >> sigma) (zeta >> tau) >> h.
Proof. fext=> A /=. by rewrite Tm.ren_inst. Qed.

Lemma tm_inst_renX {m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> tm m2 n2) (zeta : ren n2 n3) :
Tm.inst sigma tau >> Tm.ren xi zeta = Tm.inst (sigma >> Ty.ren xi) (tau >> Tm.ren xi zeta).
Proof. fext=> A /=. exact: Tm.inst_ren. Qed.

Lemma tm_inst_renR {T m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> tm m2 n2) (zeta : ren n2 n3) (h : _ -> T) :
Tm.inst sigma tau >> (Tm.ren xi zeta >> h) = Tm.inst (sigma >> Ty.ren xi) (tau >> Tm.ren xi zeta) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_ren. Qed.

Lemma tm_id_instX {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) : Tm.var >> Tm.inst sigma tau = tau.
Proof. by []. Qed.

Lemma tm_inst_idX {m n} : Tm.inst (@Ty.var m) (@Tm.var m n) = id.
Proof. fext=> A. exact: Tm.inst_id. Qed.

Lemma tm_inst_idR {T m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) (h : _ -> T) : Tm.var >> (Tm.inst sigma tau >> h) = (tau >> h).
Proof. by []. Qed.

Lemma tm_inst_compX {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> tm m2 n2) (tau2 : fin n2 -> tm m3 n3) :
Tm.inst sigma1 tau1 >> Tm.inst sigma2 tau2 = Tm.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Tm.inst sigma2 tau2).
Proof. fext=> A /=. exact: Tm.inst_comp. Qed.

Lemma tm_inst_compR {T m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> tm m2 n2) (tau2 : fin n2 -> tm m3 n3) (h : _ -> T) :
Tm.inst sigma1 tau1 >> (Tm.inst sigma2 tau2 >> h) = Tm.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Tm.inst sigma2 tau2) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_comp. Qed.

Ltac tm_simpl :=
rewrite ?tm_ren_idX ?tm_ren_compX ?tm_ren_compR
?tm_inst_renX ?tm_inst_renR
?tm_ren_instX ?tm_ren_instR
?tm_id_instX ?tm_inst_idX ?tm_inst_idR
?tm_inst_compX ?tm_inst_compR
?Tm.ren_id ?Tm.ren_comp ?Tm.ren_inst ?Tm.inst_ren ?Tm.inst_id ?Tm.inst_comp
?Tm.eval_ren ?Tm.eval_inst ?Tm.naturality
?TmVl.th2_tmE.