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.

  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.

  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.

  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.
  Canonical tm_igraded2 := Eval hnf in IGraded2 tm (@ren_tm_id).

  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).

    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.
  Canonical tm_cgraded2 := Eval hnf in CGraded2 tm (@ren_comp).

  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)).

  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).

  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.

  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.

  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.

  Lemma eval_inst {Vty : cgraded1} {Dty : graded1} {Vtm : cgraded2} {Dtm : graded2}
        (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.

  Module Exports.
    Notation tm := tm.

    Canonical tm_graded2.
    Canonical tm_cgraded2.
    Canonical tm_igraded2.
    Canonical tm_pgraded2.

    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.

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.