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.

  Unset Elimination Schemes.
  Inductive tm (m n : nat) :=
  | tvl (v : vl m n)
  | app (s : tm m n) (t : tm m n)
  | App (s : tm m n) (A : ty m)
  with vl (m n : nat) :=
  | var (i : fin n) : vl m n
  | lam (A : ty m) (b : tm m n.+1) : vl m n
  | Lam (b : tm m.+1 n) : vl m n.
  Set Elimination Schemes.
  Scheme vl_ind := Induction for vl Sort Prop
    with tm_ind := Induction for tm Sort Prop.
  Combined Scheme tv_ind from vl_ind, tm_ind.

  Arguments var {m n}, m n.

  Structure traversal (Vty Dty : nat -> Type) (Vvl Dvl Dtm : nat -> nat -> Type) := Traversal
    { tvar : forall m n, Vvl m n -> Dvl m n
    ; tlam : forall m n, Dty m -> ☐₂(fun m n => Vvl m n -> Dtm m n) m n -> Dvl m n
    ; tLam : forall m n, ☐₂(fun m n => Vty m -> Dtm m n) m n -> Dvl m n
    ; ttvl : forall m n, Dvl 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
    }.
  Arguments tvar {Vty Dty Vvl Dvl Dtm} t {m n} i.
  Arguments tlam {Vty Dty Vvl Dvl Dtm} t {m n} A F.
  Arguments tLam {Vty Dty Vvl Dvl Dtm} t {m n} F.
  Arguments ttvl {Vty Dty Vvl Dvl Dtm} t {m n} v.
  Arguments tapp {Vty Dty Vvl Dvl Dtm} t {m n} f a.
  Arguments tApp {Vty Dty Vvl Dvl Dtm} t {m n} f A.

  Fixpoint eval_vl {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm)
    {m1 n1 m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (v : vl m1 n1) : Dvl m2 n2 :=
    match v with
    | var x => tvar E (theta x)
    | lam A s => tlam E (Ty.eval T rho A) (fun _ _ xi zeta v => eval_tm T E (rho >> th1 xi) (v .: theta >> th2 xi zeta) s)
    | Lam s => tLam E (fun _ _ xi zeta v => eval_tm T E (v .: rho >> th1 xi) (theta >> th2 xi zeta) s)
    end
  with eval_tm {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm)
    {m1 n1 m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (s : tm m1 n1) : Dtm m2 n2 :=
    match s with
    | tvl v => ttvl E (eval_vl T E rho theta v)
    | app s t => tapp E (eval_tm T E rho theta s) (eval_tm T E rho theta t)
    | App s A => tApp E (eval_tm T E rho theta s) (Ty.eval T rho A)
    end.

  Structure is_natural {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (E : traversal Vty Dty Vvl Dvl Dtm) := IsNatural
    { nvar : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (i : Vvl m1 n1),
      (tvar E i) ⋅ (xi,zeta) = tvar E (i ⋅ (xi,zeta))
    ; nlam : forall m1 n1 (A : Dty m1) (F : ☐₂(fun m n => Vvl 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 : Vvl 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))
    ; ntvl : forall m1 m2 n1 n2 (xi : iren m1 m2) (zeta : iren n1 n2) (v : Dvl m1 n1),
        (ttvl E v) ⋅ (xi,zeta) = ttvl E (v ⋅ (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)
    }.

  Structure model (Vty Dty : graded1) (Vvl Dvl Dtm : graded2) := Model
    { base : traversal Vty Dty Vvl Dvl Dtm
    ; _ : is_natural base
    }.

  Local Coercion base : model >-> traversal.

  Definition model_of {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (Vty' Dty' : nat -> Type) (Vvl' Dvl' Dtm' : nat -> nat -> Type)
    of phant_id (Vty : nat -> Type) Vty' of phant_id (Dty : nat -> Type) Dty'
    of phant_id (Vvl : nat -> nat -> Type) Vvl' of phant_id (Dvl : nat -> nat -> Type) Dvl'
    of phant_id (Dtm : nat -> nat -> Type) Dtm'
    := model Vty Dty Vvl Dvl Dtm.

  Local Notation "'{' 'model' Vty ',' Dty ',' Vvl ',' Dvl ',' Dtm '}'" := (@model_of _ _ _ _ _ Vty Dty Vvl Dvl Dtm id id id id id) : type_scope.

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

  Definition ren_traversal : traversal fin ty fin2 vl 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))
              (@tvl) (@app) (@App).
  Local Notation vl_ren := (eval_vl Ty.ren_traversal ren_traversal).
  Local Notation tm_ren := (eval_tm Ty.ren_traversal ren_traversal).
  Canonical vl_graded2 := Eval hnf in Graded2 vl (@eval_vl _ _ _ _ _ Ty.ren_traversal ren_traversal).
  Canonical tm_graded2 := Eval hnf in Graded2 tm (@eval_tm _ _ _ _ _ Ty.ren_traversal ren_traversal).

  Lemma th2_vlE {m1 m2 n1 n2} (xi : iren m1 m2) (zeta : iren n1 n2) (v : vl m1 n1) :
    v ⋅ (xi, zeta) = vl_ren xi zeta v.
  Proof. by []. Qed.

  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_vlE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ _ _ (up zeta)).
    - rewrite th2_vlE /=. asimpl. f_equal. rewrite -shift_up. exact: (H _ _ _ _ _ (up xi)).
  Qed.
  Canonical ren_model : {model fin, ty, fin2, vl, tm} := Eval hnf in Model ren_is_natural.

  Lemma ren_vl_tm_id m n :
    (forall v : vl m n, vl_ren id id v = v) /\
    (forall s : tm m n, tm_ren id id s = s).
  Proof.
    move: m n. apply tv_ind => //=[m n A b ih|m n b ih|m n v->|m n s->t->|m n s->A]//.
    - asimpl. by rewrite ih.
    - asimpl. by rewrite ih.
    - by asimpl.
  Qed.

  Lemma ren_vl_id {m n : nat} (v : vl m n) : vl_ren id id v = v.
  Proof. by case: (ren_vl_tm_id m n). Qed.
  Canonical vl_igraded2 := Eval hnf in IGraded2 vl (@ren_vl_id).

  Lemma ren_tm_id {m n : nat} (s : tm m n) : tm_ren id id s = s.
  Proof. by case: (ren_vl_tm_id m n). Qed.
  Canonical tm_igraded2 := Eval hnf in IGraded2 tm (@ren_tm_id).

  Section EvalRen.
    Context {Vty : graded1} {Dty : nat -> Type} {Vvl : graded2} {Dvl Dtm : nat -> nat -> Type}
            (t1 : Ty.traversal Vty Dty) (t2 : traversal Vty Dty Vvl Dvl Dtm).

    Lemma eval_vl_tm_ren m1 n1 :
      (forall (v : vl m1 n1) m2 m3 n2 n3 (xi : ren m1 m2) (zeta : ren n1 n2) (rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3),
          eval_vl t1 t2 rho1 rho2 (vl_ren xi zeta v) = eval_vl t1 t2 (xi >> rho1) (zeta >> rho2) v) /\
      (forall (s : tm m1 n1) m2 m3 n2 n3 (xi : ren m1 m2) (zeta : ren n1 n2) (rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3),
          eval_tm t1 t2 rho1 rho2 (tm_ren xi zeta s) = eval_tm t1 t2 (xi >> rho1) (zeta >> rho2) s).
    Proof.
      move: m1 n1. apply tv_ind => //=[m n A b ih|m n b ih|m n v ih|m n s ihs t iht|m n s ih A] m2 m3 n2 n3 xi zeta rho1 rho2.
      - asimpl. f_equal;fext=> m4 n4 xi' zeta' i. rewrite ih. by asimpl.
      - f_equal;fext=> m4 n4 xi' zeta' i. rewrite ih. by asimpl.
      - by rewrite ih.
      - by rewrite ihs iht.
      - asimpl. by rewrite ih.
    Qed.

    Lemma eval_vl_ren {m1 m2 m3 n1 n2 n3} (v : vl m1 n1) (xi : ren m1 m2) (zeta : ren n1 n2)
          (rho1 : fin m2 -> Vty m3) (rho2 : fin n2 -> Vvl m3 n3) :
      eval_vl t1 t2 rho1 rho2 (vl_ren xi zeta v) = eval_vl t1 t2 (xi >> rho1) (zeta >> rho2) v.
    Proof. by case: (eval_vl_tm_ren m1 n1). Qed.

    Lemma eval_tm_ren {m1 m2 m3 n1 n2 n3} (s : tm m1 n1) (xi : ren m1 m2) (zeta : ren n1 n2)
          (rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3) :
      eval_tm t1 t2 rho theta (tm_ren xi zeta s) = eval_tm t1 t2 (xi >> rho) (zeta >> theta) s.
    Proof. by case: (eval_vl_tm_ren m1 n1). Qed.
  End EvalRen.

  Lemma ren_vl_comp {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (xi2 : ren m2 m3)
        (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) (v : vl m1 n1) :
    vl_ren xi2 zeta2 (vl_ren xi1 zeta1 v) = vl_ren (xi1 >> xi2) (zeta1 >> zeta2) v.
  Proof. exact: eval_vl_ren. Qed.
  Canonical vl_cgraded2 := Eval hnf in CGraded2 vl (@ren_vl_comp).

  Lemma ren_tm_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_tm_ren. Qed.
  Canonical tm_cgraded2 := Eval hnf in CGraded2 tm (@ren_tm_comp).

  Lemma ren_vl_tm_inj :
    forall m1 n1,
      (forall (v1 v2 : vl m1 n1) {m2 n2} (xi : ren m1 m2) (zeta : ren n1 n2),
          injective xi -> injective zeta -> vl_ren xi zeta v1 = vl_ren xi zeta v2 -> v1 = v2) /\
      (forall (s1 s2 : tm m1 n1) {m2 n2} (xi : ren m1 m2) (zeta : ren n1 n2),
          injective xi -> injective zeta -> tm_ren xi zeta s1 = tm_ren xi zeta s2 -> s1 = s2).
  Proof.
    apply tv_ind => [m1 n1 i|m1 n1 A1 b1 ih|m1 n1 b1 ih|m1 n1 v1 ih|m1 n1 s1 ihs t1 iht|m1 n1 s1 ih A1].
    - 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=> [v2||]//= m2 n2 xi zeta fP gP [/ih->].
    - 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->].
  Qed.

  Lemma ren_vl_inj {m1 m2 n1 n2} (xi : ren m1 m2) (zeta : ren n1 n2) (v1 v2 : vl m1 n1) :
    injective xi -> injective zeta -> vl_ren xi zeta v1 = vl_ren xi zeta v2 -> v1 = v2.
  Proof. case: (ren_vl_tm_inj m1 n1) => H _. exact: H. 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. case: (ren_vl_tm_inj m1 n1) => _ H. exact: H. Qed.

  Canonical vl_pgraded2 := Eval hnf in PGraded2 vl (fun m1 m2 n1 n2 xi zeta v1 v2 =>
    @ren_vl_inj m1 m2 n1 n2 xi zeta v1 v2 (@iren_inj _ _ xi) (@iren_inj _ _ zeta)).

  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} {Vvl Dvl Dtm : nat -> nat -> Type} (T : Ty.traversal Vty Dty) (E : traversal Vty Dty Vvl Dvl Dtm) : traversal Dty Dty Dvl Dvl 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 (@ttvl _ _ _ _ _ E).
    - exact (@tapp _ _ _ _ _ E).
    - exact (@tApp _ _ _ _ _ E).
  Defined.

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

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

  Definition lift_vl_tm_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
    (forall (v : vl m1 n1) {m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2),
        eval_vl T E rho theta v = eval_vl (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) v) /\
    (forall (s : tm m1 n1) {m2 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2),
        eval_tm T E rho theta s = eval_tm (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) s).
  Proof.
    move: m1 n1. apply tv_ind => //=[m1 n1 A b ih|m1 n1 b ih|m1 n1 v 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 ih.
    - by rewrite ihs iht.
    - by rewrite ihs Ty.embed.
  Qed.

  Lemma lift_vl_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) {m1 m2 n1 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (v : vl m1 n1) :
    eval_vl T E rho theta v =
    eval_vl (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) v.
  Proof. by case: (lift_vl_tm_embed T E m1 n1). Qed.

  Lemma lift_tm_embed {Vty Dty : graded1} {Vvl Dvl Dtm : graded2} (T : Ty.model Vty Dty) (E : model Vty Dty Vvl Dvl Dtm) {m1 m2 n1 n2 : nat} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (s : tm m1 n1) :
    eval_tm T E rho theta s =
    eval_tm (Ty.lift T) (lift T E) (rho >> Ty.tvar T) (theta >> tvar E) s.
  Proof. by case: (lift_vl_tm_embed T E m1 n1). Qed.

  Notation inst_traversal := (lift Ty.ren_traversal ren_traversal).
  Notation inst_vl := (eval_vl Ty.inst_traversal inst_traversal).
  Notation inst_tm := (eval_tm Ty.inst_traversal inst_traversal).
  Notation "v .[ sigma , tau ]" := (inst_vl sigma tau v)
    (at level 2, left associativity, format "v .[ sigma , tau ]") : vl_inst_scope.
  Delimit Scope vl_inst_scope with vl.
  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_vl_id {m n : nat} (v : vl m n) :
    v.[Ty.var, var]%vl = v.
  Proof.
    rewrite -{2}[v]th_id2/=. symmetry. exact: lift_vl_embed.
  Qed.

  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_tm_embed.
  Qed.

  Definition vl_ren_inst {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (zeta1 : ren n1 n2) (xi2 : fin m2 -> ty m3) (zeta2 : fin n2 -> vl m3 n3) (v : vl m1 n1) :
    (vl_ren xi1 zeta1 v).[xi2, zeta2]%vl = v.[xi1 >> xi2, zeta1 >> zeta2]%vl.
  Proof. exact: eval_vl_ren. Qed.

  Definition tm_ren_inst {m1 m2 m3 n1 n2 n3 : nat} (xi1 : ren m1 m2) (zeta1 : ren n1 n2) (xi2 : fin m2 -> ty m3) (zeta2 : fin n2 -> vl m3 n3) (s : tm m1 n1) :
    (tm_ren xi1 zeta1 s).[xi2, zeta2]%tm = s.[xi1 >> xi2, zeta1 >> zeta2]%tm.
  Proof. exact: eval_tm_ren. Qed.

  Definition naturality_vl_tm {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2} (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
    (forall (v : vl m1 n1) {m2 m3 n2 n3} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3),
        (eval_vl t1 t2 rho theta v) ⋅ (xi,zeta) = eval_vl t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) v)
    /\
    (forall (s : tm m1 n1) {m2 m3 n2 n3} (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3),
        (eval_tm t1 t2 rho theta s) ⋅ (xi,zeta) = eval_tm t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) s).
  Proof.
    move: m1 n1. apply tv_ind =>[m1 n1 i|m1 n1 A b ih|m1 n1 b ih|m1 n1 v ih|m1 n1 s ihs t iht|m1 n1 s ihs A] m2 m3 n2 n3 rho theta xi zeta.
    - exact: (nvar t2).
    - cbn. rewrite (nlam t2). f_equal. by asimpl. fext=> m4 n4 xi' zeta' i /=. by asimpl.
      intros. rewrite ih. by asimpl.
    - cbn. rewrite (nLam t2). f_equal. fext=> /=m4 n4 xi' zeta' i. by asimpl.
      intros. rewrite ih. by asimpl.
    - by rewrite/=(ntvl t2) ih.
    - by rewrite/=(napp t2) ihs iht.
    - by rewrite/=(nApp t2) ihs Ty.naturality.
  Qed.

  Lemma naturality_vl {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2}
        (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3}
        (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3)
        (v : vl m1 n1) :
    (eval_vl t1 t2 rho theta v) ⋅ (xi,zeta) = eval_vl t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) v.
  Proof. by case: (naturality_vl_tm t1 t2 m1 n1). Qed.

  Lemma naturality_tm {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2}
        (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3}
        (rho : fin m1 -> Vty m2) (theta : fin n1 -> Vvl m2 n2) (xi : iren m2 m3) (zeta : iren n2 n3)
        (s : tm m1 n1) :
    (eval_tm t1 t2 rho theta s) ⋅ (xi,zeta) = eval_tm t1 t2 (rho >> th1 xi) (theta >> th2 xi zeta) s.
  Proof. by case: (naturality_vl_tm t1 t2 m1 n1). Qed.

  Lemma eval_vl_tm_inst {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2}
        (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) (m1 n1 : nat) :
    (forall (v : vl m1 n1) {m2 m3 n2 n3 : nat} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
            (rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3),
        eval_vl t1 t2 rho theta v.[sigma, tau]%vl =
        eval_vl (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) v)
    /\
    (forall (s : tm m1 n1) {m2 m3 n2 n3 : nat} (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
            (rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3),
        eval_tm t1 t2 rho theta s.[sigma, tau]%tm =
        eval_tm (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) s).
  Proof.
    move: m1 n1. apply tv_ind => //=[m1 n1 A b ih|m1 n1 b ih|m1 n1 v 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_vl_ren. symmetry. exact: naturality_vl.
    - f_equal;fext=>/=m4 n4 sigma' tau' i. rewrite ih /=. f_equal.
      fext=>/=-[]//=j. by asimpl.
      fext=>/=j. rewrite eval_vl_ren. symmetry. exact: naturality_vl.
    - by rewrite ih.
    - by rewrite ihs iht.
    - asimpl. by rewrite ihs.
  Qed.

  Lemma eval_vl_inst {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2}
        (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3 : nat}
        (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
        (rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3)
        (v : vl m1 n1) :
    eval_vl t1 t2 rho theta v.[sigma, tau]%vl =
    eval_vl (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) v.
  Proof. by case: (eval_vl_tm_inst t1 t2 m1 n1). Qed.

  Lemma eval_tm_inst {Vty : cgraded1} {Dty : graded1} {Vvl : cgraded2} {Dvl Dtm : graded2}
        (t1 : Ty.model Vty Dty) (t2 : model Vty Dty Vvl Dvl Dtm) {m1 m2 m3 n1 n2 n3 : nat}
        (sigma : fin m1 -> ty m2) (tau : fin n1 -> vl m2 n2)
        (rho : fin m2 -> Vty m3) (theta : fin n2 -> Vvl m3 n3)
        (s : tm m1 n1) :
    eval_tm t1 t2 rho theta s.[sigma, tau]%tm =
    eval_tm (Ty.lift t1) (lift t1 t2) (sigma >> Ty.eval t1 rho) (tau >> eval_vl t1 t2 rho theta) s.
  Proof. by case: (eval_vl_tm_inst t1 t2 m1 n1). Qed.

  Lemma inst_vl_comp {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2)
        (sigma2 : fin m2 -> ty m3) (tau2 : fin n2 -> vl m3 n3) (v : vl m1 n1) :
    v.[sigma1,tau1]%vl.[sigma2,tau2]%vl = v.[sigma1 >> Ty.inst sigma2, tau1 >> inst_vl sigma2 tau2]%vl.
  Proof. exact: eval_vl_inst. Qed.

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

  Lemma vl_inst_ren {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2) (sigma2 : ren m2 m3) (tau2 : ren n2 n3) (v : vl m1 n1) :
    vl_ren sigma2 tau2 v.[sigma1,tau1]%vl = v.[sigma1 >> Ty.ren sigma2, tau1 >> vl_ren sigma2 tau2]%vl.
  Proof.
    rewrite lift_vl_embed inst_vl_comp. f_equal; fext => i /=; symmetry.
    exact: Ty.embed. exact: lift_vl_embed.
  Qed.

  Lemma tm_inst_ren {m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (tau1 : fin n1 -> vl m2 n2) (sigma2 : ren m2 m3) (tau2 : ren n2 n3) (s : tm m1 n1) :
    tm_ren sigma2 tau2 s.[sigma1,tau1]%tm = s.[sigma1 >> Ty.ren sigma2, tau1 >> vl_ren sigma2 tau2]%tm.
  Proof.
    rewrite lift_tm_embed inst_tm_comp. f_equal; fext => i /=; symmetry.
    exact: Ty.embed. exact: lift_vl_embed.
  Qed.

  End Defs.

  Module Exports.
    Notation vl := vl.
    Notation tm := tm.

    Canonical vl_graded2.
    Canonical vl_cgraded2.
    Canonical vl_igraded2.
    Canonical vl_pgraded2.
    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 Vvl Dvl Dtm} t {m n} i.
    Arguments tlam {Vty Dty Vvl Dvl Dtm} t {m n} A F.
    Arguments tLam {Vty Dty Vvl Dvl Dtm} t {m n} F.
    Arguments ttvl {Vty Dty Vvl Dvl Dtm} t {m n} v.
    Arguments tapp {Vty Dty Vvl Dvl Dtm} t {m n} xi a.
    Arguments tApp {Vty Dty Vvl Dvl Dtm} t {m n} xi A.

    Module FCBV.
      Notation traversal := traversal.
      Notation Traversal := Traversal.
      Notation tvar := tvar.
      Notation tlam := tlam.
      Notation tLam := tLam.
      Notation ttvl := ttvl.
      Notation tapp := tapp.
      Notation tApp := tApp.

      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 ntvl := ntvl.
      Notation napp := napp.
      Notation nApp := nApp.

      Notation model := model.
    End FCBV.

    Module Vl.
      (* Types *)
      Notation var := var.
      Notation lam := lam.
      Notation Lam := Lam.

      (* Evaluation *)
      Notation eval := eval_vl.

      Notation eval_ren := eval_vl_ren.
      Notation eval_inst := eval_vl_inst.
      Notation naturality := naturality_vl.

      Notation embed := lift_vl_embed.

      (* Renaming *)
      Notation ren := (eval_vl Ty.ren_traversal FCBV.ren_traversal).

      Notation ren_id := ren_vl_id.
      Notation ren_comp := ren_vl_comp.
      Notation ren_inj := ren_vl_inj.

      (* Instantiation *)
      Notation inst := (eval_vl Ty.inst_traversal FCBV.inst_traversal).

      Notation ren_inst := vl_ren_inst.
      Notation inst_ren := vl_inst_ren.

      Notation inst_id := inst_vl_id.
      Notation inst_comp := inst_vl_comp.
    End Vl.

    Module Tm.
      (* Types *)
      Notation tvl := tvl.
      Notation app := app.
      Notation App := App.

      (* Evaluation *)
      Notation eval := eval_tm.

      Notation eval_ren := eval_tm_ren.
      Notation eval_inst := eval_tm_inst.
      Notation naturality := naturality_tm.

      Notation embed := lift_tm_embed.

      (* Renaming *)
      Notation ren := (eval_tm Ty.ren_traversal FCBV.ren_traversal).

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

      (* Instantiation *)
      Notation inst := (eval_tm Ty.inst_traversal FCBV.inst_traversal).

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

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

    Notation "v ◁ ( xi , zeta )" := (Vl.ren xi zeta v) (at level 50,
      format "v ◁ ( xi , zeta )") : vl_inst_scope.

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

    Notation "v .[ sigma , tau ]" := (Vl.inst sigma tau v)
      (at level 2, left associativity, format "v .[ sigma , tau ]") : vl_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 vl_inst_scope with vl.
    Delimit Scope tm_inst_scope with tm.
  End Exports.

End TmVl.
Export TmVl.Exports.

Lemma vl_ren_idX {m n} : Vl.ren (id : fin m -> fin m) (id : fin n -> fin n) = id.
Proof. fext=> A. exact: Vl.ren_id. Qed.

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 vl_ren_compX {m1 m2 m3 n1 n2 n3} (xi1 : ren m1 m2) (xi2 : ren m2 m3) (zeta1 : ren n1 n2) (zeta2 : ren n2 n3) :
  Vl.ren xi1 zeta1 >> Vl.ren xi2 zeta2 = Vl.ren (xi1 >> xi2) (zeta1 >> zeta2).
Proof. fext=> A /=. exact: Vl.ren_comp. 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 vl_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) :
  Vl.ren xi1 zeta1 >> (Vl.ren xi2 zeta2 >> h) = Vl.ren (xi1 >> xi2) (zeta1 >> zeta2) >> h.
Proof. fext=> A /=. by rewrite Vl.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 vl_ren_instX {m1 m2 m3 n1 n2 n3} (xi : ren m1 m2) (sigma : fin m2 -> ty m3) (zeta : ren n1 n2) (tau : fin n2 -> vl m3 n3) :
  Vl.ren xi zeta >> Vl.inst sigma tau = Vl.inst (xi >> sigma) (zeta >> tau).
Proof. fext=> A /=. exact: Vl.ren_inst. 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 -> vl 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 vl_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 -> vl m3 n3) (h : _ -> T) :
  Vl.ren xi zeta >> (Vl.inst sigma tau >> h) = Vl.inst (xi >> sigma) (zeta >> tau) >> h.
Proof. fext=> A /=. by rewrite Vl.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 -> vl 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 vl_inst_renX {m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) :
  Vl.inst sigma tau >> Vl.ren xi zeta = Vl.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta).
Proof. fext=> A /=. exact: Vl.inst_ren. Qed.

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

Lemma vl_inst_renR {T m1 m2 m3 n1 n2 n3} (sigma : fin m1 -> ty m2) (xi : ren m2 m3) (tau : fin n1 -> vl m2 n2) (zeta : ren n2 n3) (h : _ -> T) :
  Vl.inst sigma tau >> (Vl.ren xi zeta >> h) = Vl.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta) >> h.
Proof. fext=> A /=. by rewrite Vl.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 -> vl m2 n2) (zeta : ren n2 n3) (h : _ -> T) :
  Tm.inst sigma tau >> (Tm.ren xi zeta >> h) = Tm.inst (sigma >> Ty.ren xi) (tau >> Vl.ren xi zeta) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_ren. Qed.

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

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

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

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

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

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

Lemma vl_inst_compR {T m1 m2 m3 n1 n2 n3} (sigma1 : fin m1 -> ty m2) (sigma2 : fin m2 -> ty m3) (tau1 : fin n1 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) (h : _ -> T) :
  Vl.inst sigma1 tau1 >> (Vl.inst sigma2 tau2 >> h) = Vl.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2) >> h.
Proof. fext=> A /=. by rewrite Vl.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 -> vl m2 n2) (tau2 : fin n2 -> vl m3 n3) (h : _ -> T) :
  Tm.inst sigma1 tau1 >> (Tm.inst sigma2 tau2 >> h) = Tm.inst (sigma1 >> Ty.inst sigma2) (tau1 >> Vl.inst sigma2 tau2) >> h.
Proof. fext=> A /=. by rewrite Tm.inst_comp. Qed.

Ltac vt_simpl :=
  rewrite ?vl_ren_idX ?vl_ren_compX ?vl_ren_compR
          ?tm_ren_idX ?tm_ren_compX ?tm_ren_compR
          ?vl_inst_renX ?vl_inst_renR
          ?tm_inst_renX ?tm_inst_renR
          ?vl_ren_instX ?vl_ren_instR
          ?tm_ren_instX ?tm_ren_instR
          ?vl_id_instX ?vl_inst_idX ?vl_inst_idR
          ?tm_inst_idX
          ?vl_inst_compX ?vl_inst_compR
          ?tm_inst_compX ?tm_inst_compR
          ?Vl.ren_id ?Vl.ren_comp ?Vl.ren_inst ?Vl.inst_ren ?Vl.inst_id ?Vl.inst_comp
          ?Tm.ren_id ?Tm.ren_comp ?Tm.ren_inst ?Tm.inst_ren ?Tm.inst_id ?Tm.inst_comp
          ?Vl.eval_ren ?Vl.eval_inst ?Vl.naturality
          ?Tm.eval_ren ?Tm.eval_inst ?Tm.naturality
          ?TmVl.th2_vlE ?TmVl.th2_tmE.