Require Export fintype. Require Export header_extensible.

Section ty.
Inductive ty (nty : nat) : Type :=
  | var_ty : (fin) (nty) -> ty (nty)
  | arr : ty (nty) -> ty (nty) -> ty (nty)
  | all : ty ((S) nty) -> ty (nty).

Lemma congr_arr { mty : nat } { s0 : ty (mty) } { s1 : ty (mty) } { t0 : ty (mty) } { t1 : ty (mty) } (H1 : s0 = t0) (H2 : s1 = t1) : arr (mty) s0 s1 = arr (mty) t0 t1 .
Proof. congruence. Qed.

Lemma congr_all { mty : nat } { s0 : ty ((S) mty) } { t0 : ty ((S) mty) } (H1 : s0 = t0) : all (mty) s0 = all (mty) t0 .
Proof. congruence. Qed.

Definition upRen_ty_ty { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) ((S) (m)) -> (fin) ((S) (n)) :=
  (up_ren) xi.

Definition upRenList_ty_ty (p : nat) { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (p+ (m)) -> (fin) (p+ (n)) :=
  upRen_p p xi.

Fixpoint ren_ty { mty : nat } { nty : nat } (xity : (fin) (mty) -> (fin) (nty)) (s : ty (mty)) : ty (nty) :=
    match s with
    | var_ty (_) s => (var_ty (nty)) (xity s)
    | arr (_) s0 s1 => arr (nty) ((ren_ty xity) s0) ((ren_ty xity) s1)
    | all (_) s0 => all (nty) ((ren_ty (upRen_ty_ty xity)) s0)
    end.

Definition up_ty_ty { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) : (fin) ((S) (m)) -> ty ((S) nty) :=
  (scons) ((var_ty ((S) nty)) (var_zero)) ((funcomp) (ren_ty (shift)) sigma).

Definition upList_ty_ty (p : nat) { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) : (fin) (p+ (m)) -> ty (p+ nty) :=
  scons_p p ((funcomp) (var_ty (p+ nty)) (zero_p p)) ((funcomp) (ren_ty (shift_p p)) sigma).

Fixpoint subst_ty { mty : nat } { nty : nat } (sigmaty : (fin) (mty) -> ty (nty)) (s : ty (mty)) : ty (nty) :=
    match s with
    | var_ty (_) s => sigmaty s
    | arr (_) s0 s1 => arr (nty) ((subst_ty sigmaty) s0) ((subst_ty sigmaty) s1)
    | all (_) s0 => all (nty) ((subst_ty (up_ty_ty sigmaty)) s0)
    end.

Definition upId_ty_ty { mty : nat } (sigma : (fin) (mty) -> ty (mty)) (Eq : forall x, sigma x = (var_ty (mty)) x) : forall x, (up_ty_ty sigma) x = (var_ty ((S) mty)) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_ty (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upIdList_ty_ty { p : nat } { mty : nat } (sigma : (fin) (mty) -> ty (mty)) (Eq : forall x, sigma x = (var_ty (mty)) x) : forall x, (upList_ty_ty p sigma) x = (var_ty (p+ mty)) x :=
  fun n => scons_p_eta (var_ty (p+ mty)) (fun n => (ap) (ren_ty (shift_p p)) (Eq n)) (fun n => eq_refl).

Fixpoint idSubst_ty { mty : nat } (sigmaty : (fin) (mty) -> ty (mty)) (Eqty : forall x, sigmaty x = (var_ty (mty)) x) (s : ty (mty)) : subst_ty sigmaty s = s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((idSubst_ty sigmaty Eqty) s0) ((idSubst_ty sigmaty Eqty) s1)
    | all (_) s0 => congr_all ((idSubst_ty (up_ty_ty sigmaty) (upId_ty_ty (_) Eqty)) s0)
    end.

Definition upExtRen_ty_ty { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_ty_ty xi) x = (upRen_ty_ty zeta) x :=
  fun n => match n with
  | Some fin_n => (ap) (shift) (Eq fin_n)
  | None => eq_refl
  end.

Definition upExtRen_list_ty_ty { 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, (upRenList_ty_ty p xi) x = (upRenList_ty_ty p zeta) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (shift_p p) (Eq n)).

Fixpoint extRen_ty { mty : nat } { nty : nat } (xity : (fin) (mty) -> (fin) (nty)) (zetaty : (fin) (mty) -> (fin) (nty)) (Eqty : forall x, xity x = zetaty x) (s : ty (mty)) : ren_ty xity s = ren_ty zetaty s :=
    match s with
    | var_ty (_) s => (ap) (var_ty (nty)) (Eqty s)
    | arr (_) s0 s1 => congr_arr ((extRen_ty xity zetaty Eqty) s0) ((extRen_ty xity zetaty Eqty) s1)
    | all (_) s0 => congr_all ((extRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upExtRen_ty_ty (_) (_) Eqty)) s0)
    end.

Definition upExt_ty_ty { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) (tau : (fin) (m) -> ty (nty)) (Eq : forall x, sigma x = tau x) : forall x, (up_ty_ty sigma) x = (up_ty_ty tau) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_ty (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upExt_list_ty_ty { p : nat } { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) (tau : (fin) (m) -> ty (nty)) (Eq : forall x, sigma x = tau x) : forall x, (upList_ty_ty p sigma) x = (upList_ty_ty p tau) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (ren_ty (shift_p p)) (Eq n)).

Fixpoint ext_ty { mty : nat } { nty : nat } (sigmaty : (fin) (mty) -> ty (nty)) (tauty : (fin) (mty) -> ty (nty)) (Eqty : forall x, sigmaty x = tauty x) (s : ty (mty)) : subst_ty sigmaty s = subst_ty tauty s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((ext_ty sigmaty tauty Eqty) s0) ((ext_ty sigmaty tauty Eqty) s1)
    | all (_) s0 => congr_all ((ext_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (upExt_ty_ty (_) (_) Eqty)) s0)
    end.

Definition up_ren_ren_ty_ty { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_ty_ty tau) (upRen_ty_ty xi)) x = (upRen_ty_ty theta) x :=
  up_ren_ren xi tau theta Eq.

Definition up_ren_ren_list_ty_ty { p : nat } { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRenList_ty_ty p tau) (upRenList_ty_ty p xi)) x = (upRenList_ty_ty p theta) x :=
  up_ren_ren_p Eq.

Fixpoint compRenRen_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) (rhoty : (fin) (mty) -> (fin) (lty)) (Eqty : forall x, ((funcomp) zetaty xity) x = rhoty x) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty rhoty s :=
    match s with
    | var_ty (_) s => (ap) (var_ty (lty)) (Eqty s)
    | arr (_) s0 s1 => congr_arr ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_ty xity zetaty rhoty Eqty) s1)
    | all (_) s0 => congr_all ((compRenRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upRen_ty_ty rhoty) (up_ren_ren (_) (_) (_) Eqty)) s0)
    end.

Definition up_ren_subst_ty_ty { k : nat } { l : nat } { mty : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_ty_ty tau) (upRen_ty_ty xi)) x = (up_ty_ty theta) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_ty (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition up_ren_subst_list_ty_ty { p : nat } { k : nat } { l : nat } { mty : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_ty_ty p tau) (upRenList_ty_ty p xi)) x = (upList_ty_ty p theta) x :=
  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_ty (shift_p p)) (Eq z)))).

Fixpoint compRenSubst_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (tauty : (fin) (kty) -> ty (lty)) (thetaty : (fin) (mty) -> ty (lty)) (Eqty : forall x, ((funcomp) tauty xity) x = thetaty x) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty thetaty s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_ty xity tauty thetaty Eqty) s1)
    | all (_) s0 => congr_all ((compRenSubst_ty (upRen_ty_ty xity) (up_ty_ty tauty) (up_ty_ty thetaty) (up_ren_subst_ty_ty (_) (_) (_) Eqty)) s0)
    end.

Definition up_subst_ren_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (zetaty : (fin) (lty) -> (fin) (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (ren_ty zetaty) sigma) x = theta x) : forall x, ((funcomp) (ren_ty (upRen_ty_ty zetaty)) (up_ty_ty sigma)) x = (up_ty_ty theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenRen_ty (shift) (upRen_ty_ty zetaty) ((funcomp) (shift) zetaty) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compRenRen_ty zetaty (shift) ((funcomp) (shift) zetaty) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_ty (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_ren_list_ty_ty { p : nat } { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (zetaty : (fin) (lty) -> (fin) (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (ren_ty zetaty) sigma) x = theta x) : forall x, ((funcomp) (ren_ty (upRenList_ty_ty p zetaty)) (upList_ty_ty p sigma)) x = (upList_ty_ty p theta) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (_) n) (scons_p_congr (fun x => (ap) (var_ty (p+ mty)) (scons_p_head' (_) (_) x)) (fun n => (eq_trans) (compRenRen_ty (shift_p p) (upRenList_ty_ty p zetaty) ((funcomp) (shift_p p) zetaty) (fun x => scons_p_tail' (_) (_) x) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_ty zetaty (shift_p p) ((funcomp) (shift_p p) zetaty) (fun x => eq_refl) (sigma n))) ((ap) (ren_ty (shift_p p)) (Eq n))))).

Fixpoint compSubstRen_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) (thetaty : (fin) (mty) -> ty (lty)) (Eqty : forall x, ((funcomp) (ren_ty zetaty) sigmaty) x = thetaty x) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty thetaty s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s1)
    | all (_) s0 => congr_all ((compSubstRen_ty (up_ty_ty sigmaty) (upRen_ty_ty zetaty) (up_ty_ty thetaty) (up_subst_ren_ty_ty (_) (_) (_) Eqty)) s0)
    end.

Definition up_subst_subst_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (tauty : (fin) (lty) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (subst_ty tauty) sigma) x = theta x) : forall x, ((funcomp) (subst_ty (up_ty_ty tauty)) (up_ty_ty sigma)) x = (up_ty_ty theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenSubst_ty (shift) (up_ty_ty tauty) ((funcomp) (up_ty_ty tauty) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_ty tauty (shift) ((funcomp) (ren_ty (shift)) tauty) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_ty (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_subst_list_ty_ty { p : nat } { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (tauty : (fin) (lty) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (subst_ty tauty) sigma) x = theta x) : forall x, ((funcomp) (subst_ty (upList_ty_ty p tauty)) (upList_ty_ty p sigma)) x = (upList_ty_ty p theta) x :=
  fun n => (eq_trans) (scons_p_comp' ((funcomp) (var_ty (p+ lty)) (zero_p p)) (_) (_) n) (scons_p_congr (fun x => scons_p_head' (_) (fun z => ren_ty (shift_p p) (_)) x) (fun n => (eq_trans) (compRenSubst_ty (shift_p p) (upList_ty_ty p tauty) ((funcomp) (upList_ty_ty p tauty) (shift_p p)) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_ty tauty (shift_p p) (_) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (sigma n))) ((ap) (ren_ty (shift_p p)) (Eq n))))).

Fixpoint compSubstSubst_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (tauty : (fin) (kty) -> ty (lty)) (thetaty : (fin) (mty) -> ty (lty)) (Eqty : forall x, ((funcomp) (subst_ty tauty) sigmaty) x = thetaty x) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty thetaty s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s1)
    | all (_) s0 => congr_all ((compSubstSubst_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (up_ty_ty thetaty) (up_subst_subst_ty_ty (_) (_) (_) Eqty)) s0)
    end.

Definition rinstInst_up_ty_ty { m : nat } { nty : nat } (xi : (fin) (m) -> (fin) (nty)) (sigma : (fin) (m) -> ty (nty)) (Eq : forall x, ((funcomp) (var_ty (nty)) xi) x = sigma x) : forall x, ((funcomp) (var_ty ((S) nty)) (upRen_ty_ty xi)) x = (up_ty_ty sigma) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_ty (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition rinstInst_up_list_ty_ty { p : nat } { m : nat } { nty : nat } (xi : (fin) (m) -> (fin) (nty)) (sigma : (fin) (m) -> ty (nty)) (Eq : forall x, ((funcomp) (var_ty (nty)) xi) x = sigma x) : forall x, ((funcomp) (var_ty (p+ nty)) (upRenList_ty_ty p xi)) x = (upList_ty_ty p sigma) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (var_ty (p+ nty)) n) (scons_p_congr (fun z => eq_refl) (fun n => (ap) (ren_ty (shift_p p)) (Eq n))).

Fixpoint rinst_inst_ty { mty : nat } { nty : nat } (xity : (fin) (mty) -> (fin) (nty)) (sigmaty : (fin) (mty) -> ty (nty)) (Eqty : forall x, ((funcomp) (var_ty (nty)) xity) x = sigmaty x) (s : ty (mty)) : ren_ty xity s = subst_ty sigmaty s :=
    match s with
    | var_ty (_) s => Eqty s
    | arr (_) s0 s1 => congr_arr ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_ty xity sigmaty Eqty) s1)
    | all (_) s0 => congr_all ((rinst_inst_ty (upRen_ty_ty xity) (up_ty_ty sigmaty) (rinstInst_up_ty_ty (_) (_) Eqty)) s0)
    end.

Lemma rinstInst_ty { mty : nat } { nty : nat } (xity : (fin) (mty) -> (fin) (nty)) : ren_ty xity = subst_ty ((funcomp) (var_ty (nty)) xity) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_ty xity (_) (fun n => eq_refl) x)). Qed.

Lemma instId_ty { mty : nat } : subst_ty (var_ty (mty)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_ty (var_ty (mty)) (fun n => eq_refl) ((id) x))). Qed.

Lemma rinstId_ty { mty : nat } : @ren_ty (mty) (mty) (id) = id .
Proof. exact ((eq_trans) (rinstInst_ty ((id) (_))) instId_ty). Qed.

Lemma varL_ty { mty : nat } { nty : nat } (sigmaty : (fin) (mty) -> ty (nty)) : (funcomp) (subst_ty sigmaty) (var_ty (mty)) = sigmaty .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma varLRen_ty { mty : nat } { nty : nat } (xity : (fin) (mty) -> (fin) (nty)) : (funcomp) (ren_ty xity) (var_ty (mty)) = (funcomp) (var_ty (nty)) xity .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma compComp_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (tauty : (fin) (kty) -> ty (lty)) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty ((funcomp) (subst_ty tauty) sigmaty) s .
Proof. exact (compSubstSubst_ty sigmaty tauty (_) (fun n => eq_refl) s). Qed.

Lemma compComp'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (tauty : (fin) (kty) -> ty (lty)) : (funcomp) (subst_ty tauty) (subst_ty sigmaty) = subst_ty ((funcomp) (subst_ty tauty) sigmaty) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_ty sigmaty tauty n)). Qed.

Lemma compRen_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty ((funcomp) (ren_ty zetaty) sigmaty) s .
Proof. exact (compSubstRen_ty sigmaty zetaty (_) (fun n => eq_refl) s). Qed.

Lemma compRen'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : (fin) (mty) -> ty (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) : (funcomp) (ren_ty zetaty) (subst_ty sigmaty) = subst_ty ((funcomp) (ren_ty zetaty) sigmaty) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_ty sigmaty zetaty n)). Qed.

Lemma renComp_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (tauty : (fin) (kty) -> ty (lty)) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty ((funcomp) tauty xity) s .
Proof. exact (compRenSubst_ty xity tauty (_) (fun n => eq_refl) s). Qed.

Lemma renComp'_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (tauty : (fin) (kty) -> ty (lty)) : (funcomp) (subst_ty tauty) (ren_ty xity) = subst_ty ((funcomp) tauty xity) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_ty xity tauty n)). Qed.

Lemma renRen_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty ((funcomp) zetaty xity) s .
Proof. exact (compRenRen_ty xity zetaty (_) (fun n => eq_refl) s). Qed.

Lemma renRen'_ty { kty : nat } { lty : nat } { mty : nat } (xity : (fin) (mty) -> (fin) (kty)) (zetaty : (fin) (kty) -> (fin) (lty)) : (funcomp) (ren_ty zetaty) (ren_ty xity) = ren_ty ((funcomp) zetaty xity) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_ty xity zetaty n)). Qed.

End ty.

Section tmvl.
Inductive tm (nty nvl : nat) : Type :=
  | app : tm (nty) (nvl) -> tm (nty) (nvl) -> tm (nty) (nvl)
  | tapp : tm (nty) (nvl) -> ty (nty) -> tm (nty) (nvl)
  | vt : vl (nty) (nvl) -> tm (nty) (nvl)
 with vl (nty nvl : nat) : Type :=
  | var_vl : (fin) (nvl) -> vl (nty) (nvl)
  | lam : ty (nty) -> tm (nty) ((S) nvl) -> vl (nty) (nvl)
  | tlam : tm ((S) nty) (nvl) -> vl (nty) (nvl).

Lemma congr_app { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : tm (mty) (mvl) } { t0 : tm (mty) (mvl) } { t1 : tm (mty) (mvl) } (H1 : s0 = t0) (H2 : s1 = t1) : app (mty) (mvl) s0 s1 = app (mty) (mvl) t0 t1 .
Proof. congruence. Qed.

Lemma congr_tapp { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : ty (mty) } { t0 : tm (mty) (mvl) } { t1 : ty (mty) } (H1 : s0 = t0) (H2 : s1 = t1) : tapp (mty) (mvl) s0 s1 = tapp (mty) (mvl) t0 t1 .
Proof. congruence. Qed.

Lemma congr_vt { mty mvl : nat } { s0 : vl (mty) (mvl) } { t0 : vl (mty) (mvl) } (H1 : s0 = t0) : vt (mty) (mvl) s0 = vt (mty) (mvl) t0 .
Proof. congruence. Qed.

Lemma congr_lam { mty mvl : nat } { s0 : ty (mty) } { s1 : tm (mty) ((S) mvl) } { t0 : ty (mty) } { t1 : tm (mty) ((S) mvl) } (H1 : s0 = t0) (H2 : s1 = t1) : lam (mty) (mvl) s0 s1 = lam (mty) (mvl) t0 t1 .
Proof. congruence. Qed.

Lemma congr_tlam { mty mvl : nat } { s0 : tm ((S) mty) (mvl) } { t0 : tm ((S) mty) (mvl) } (H1 : s0 = t0) : tlam (mty) (mvl) s0 = tlam (mty) (mvl) t0 .
Proof. congruence. Qed.

Definition upRen_ty_vl { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (m) -> (fin) (n) :=
  xi.

Definition upRen_vl_ty { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (m) -> (fin) (n) :=
  xi.

Definition upRen_vl_vl { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) ((S) (m)) -> (fin) ((S) (n)) :=
  (up_ren) xi.

Definition upRenList_ty_vl (p : nat) { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (m) -> (fin) (n) :=
  xi.

Definition upRenList_vl_ty (p : nat) { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (m) -> (fin) (n) :=
  xi.

Definition upRenList_vl_vl (p : nat) { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) (p+ (m)) -> (fin) (p+ (n)) :=
  upRen_p p xi.

Fixpoint ren_tm { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (s : tm (mty) (mvl)) : tm (nty) (nvl) :=
    match s with
    | app (_) (_) s0 s1 => app (nty) (nvl) ((ren_tm xity xivl) s0) ((ren_tm xity xivl) s1)
    | tapp (_) (_) s0 s1 => tapp (nty) (nvl) ((ren_tm xity xivl) s0) ((ren_ty xity) s1)
    | vt (_) (_) s0 => vt (nty) (nvl) ((ren_vl xity xivl) s0)
    end
 with ren_vl { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (s : vl (mty) (mvl)) : vl (nty) (nvl) :=
    match s with
    | var_vl (_) (_) s => (var_vl (nty) (nvl)) (xivl s)
    | lam (_) (_) s0 s1 => lam (nty) (nvl) ((ren_ty xity) s0) ((ren_tm (upRen_vl_ty xity) (upRen_vl_vl xivl)) s1)
    | tlam (_) (_) s0 => tlam (nty) (nvl) ((ren_tm (upRen_ty_ty xity) (upRen_ty_vl xivl)) s0)
    end.

Definition up_ty_vl { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) : (fin) (m) -> vl ((S) nty) (nvl) :=
  (funcomp) (ren_vl (shift) (id)) sigma.

Definition up_vl_ty { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) : (fin) (m) -> ty (nty) :=
  (funcomp) (ren_ty (id)) sigma.

Definition up_vl_vl { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) : (fin) ((S) (m)) -> vl (nty) ((S) nvl) :=
  (scons) ((var_vl (nty) ((S) nvl)) (var_zero)) ((funcomp) (ren_vl (id) (shift)) sigma).

Definition upList_ty_vl (p : nat) { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) : (fin) (m) -> vl (p+ nty) (nvl) :=
  (funcomp) (ren_vl (shift_p p) (id)) sigma.

Definition upList_vl_ty (p : nat) { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) : (fin) (m) -> ty (nty) :=
  (funcomp) (ren_ty (id)) sigma.

Definition upList_vl_vl (p : nat) { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) : (fin) (p+ (m)) -> vl (nty) (p+ nvl) :=
  scons_p p ((funcomp) (var_vl (nty) (p+ nvl)) (zero_p p)) ((funcomp) (ren_vl (id) (shift_p p)) sigma).

Fixpoint subst_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (s : tm (mty) (mvl)) : tm (nty) (nvl) :=
    match s with
    | app (_) (_) s0 s1 => app (nty) (nvl) ((subst_tm sigmaty sigmavl) s0) ((subst_tm sigmaty sigmavl) s1)
    | tapp (_) (_) s0 s1 => tapp (nty) (nvl) ((subst_tm sigmaty sigmavl) s0) ((subst_ty sigmaty) s1)
    | vt (_) (_) s0 => vt (nty) (nvl) ((subst_vl sigmaty sigmavl) s0)
    end
 with subst_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (s : vl (mty) (mvl)) : vl (nty) (nvl) :=
    match s with
    | var_vl (_) (_) s => sigmavl s
    | lam (_) (_) s0 s1 => lam (nty) (nvl) ((subst_ty sigmaty) s0) ((subst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl)) s1)
    | tlam (_) (_) s0 => tlam (nty) (nvl) ((subst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl)) s0)
    end.

Definition upId_ty_vl { mty mvl : nat } (sigma : (fin) (mvl) -> vl (mty) (mvl)) (Eq : forall x, sigma x = (var_vl (mty) (mvl)) x) : forall x, (up_ty_vl sigma) x = (var_vl ((S) mty) (mvl)) x :=
  fun n => (ap) (ren_vl (shift) (id)) (Eq n).

Definition upId_vl_ty { mty : nat } (sigma : (fin) (mty) -> ty (mty)) (Eq : forall x, sigma x = (var_ty (mty)) x) : forall x, (up_vl_ty sigma) x = (var_ty (mty)) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition upId_vl_vl { mty mvl : nat } (sigma : (fin) (mvl) -> vl (mty) (mvl)) (Eq : forall x, sigma x = (var_vl (mty) (mvl)) x) : forall x, (up_vl_vl sigma) x = (var_vl (mty) ((S) mvl)) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_vl (id) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upIdList_ty_vl { p : nat } { mty mvl : nat } (sigma : (fin) (mvl) -> vl (mty) (mvl)) (Eq : forall x, sigma x = (var_vl (mty) (mvl)) x) : forall x, (upList_ty_vl p sigma) x = (var_vl (p+ mty) (mvl)) x :=
  fun n => (ap) (ren_vl (shift_p p) (id)) (Eq n).

Definition upIdList_vl_ty { p : nat } { mty : nat } (sigma : (fin) (mty) -> ty (mty)) (Eq : forall x, sigma x = (var_ty (mty)) x) : forall x, (upList_vl_ty p sigma) x = (var_ty (mty)) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition upIdList_vl_vl { p : nat } { mty mvl : nat } (sigma : (fin) (mvl) -> vl (mty) (mvl)) (Eq : forall x, sigma x = (var_vl (mty) (mvl)) x) : forall x, (upList_vl_vl p sigma) x = (var_vl (mty) (p+ mvl)) x :=
  fun n => scons_p_eta (var_vl (mty) (p+ mvl)) (fun n => (ap) (ren_vl (id) (shift_p p)) (Eq n)) (fun n => eq_refl).

Fixpoint idSubst_tm { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (mty)) (sigmavl : (fin) (mvl) -> vl (mty) (mvl)) (Eqty : forall x, sigmaty x = (var_ty (mty)) x) (Eqvl : forall x, sigmavl x = (var_vl (mty) (mvl)) x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((idSubst_tm sigmaty sigmavl Eqty Eqvl) s0) ((idSubst_tm sigmaty sigmavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((idSubst_tm sigmaty sigmavl Eqty Eqvl) s0) ((idSubst_ty sigmaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((idSubst_vl sigmaty sigmavl Eqty Eqvl) s0)
    end
 with idSubst_vl { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (mty)) (sigmavl : (fin) (mvl) -> vl (mty) (mvl)) (Eqty : forall x, sigmaty x = (var_ty (mty)) x) (Eqvl : forall x, sigmavl x = (var_vl (mty) (mvl)) x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((idSubst_ty sigmaty Eqty) s0) ((idSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upId_vl_ty (_) Eqty) (upId_vl_vl (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((idSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upId_ty_ty (_) Eqty) (upId_ty_vl (_) Eqvl)) s0)
    end.

Definition upExtRen_ty_vl { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_ty_vl xi) x = (upRen_ty_vl zeta) x :=
  fun n => Eq n.

Definition upExtRen_vl_ty { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_vl_ty xi) x = (upRen_vl_ty zeta) x :=
  fun n => Eq n.

Definition upExtRen_vl_vl { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_vl_vl xi) x = (upRen_vl_vl zeta) x :=
  fun n => match n with
  | Some fin_n => (ap) (shift) (Eq fin_n)
  | None => eq_refl
  end.

Definition upExtRen_list_ty_vl { 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, (upRenList_ty_vl p xi) x = (upRenList_ty_vl p zeta) x :=
  fun n => Eq n.

Definition upExtRen_list_vl_ty { 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, (upRenList_vl_ty p xi) x = (upRenList_vl_ty p zeta) x :=
  fun n => Eq n.

Definition upExtRen_list_vl_vl { 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, (upRenList_vl_vl p xi) x = (upRenList_vl_vl p zeta) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (shift_p p) (Eq n)).

Fixpoint extRen_tm { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (zetaty : (fin) (mty) -> (fin) (nty)) (zetavl : (fin) (mvl) -> (fin) (nvl)) (Eqty : forall x, xity x = zetaty x) (Eqvl : forall x, xivl x = zetavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = ren_tm zetaty zetavl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((extRen_tm xity xivl zetaty zetavl Eqty Eqvl) s0) ((extRen_tm xity xivl zetaty zetavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((extRen_tm xity xivl zetaty zetavl Eqty Eqvl) s0) ((extRen_ty xity zetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((extRen_vl xity xivl zetaty zetavl Eqty Eqvl) s0)
    end
 with extRen_vl { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (zetaty : (fin) (mty) -> (fin) (nty)) (zetavl : (fin) (mvl) -> (fin) (nvl)) (Eqty : forall x, xity x = zetaty x) (Eqvl : forall x, xivl x = zetavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = ren_vl zetaty zetavl s :=
    match s with
    | var_vl (_) (_) s => (ap) (var_vl (nty) (nvl)) (Eqvl s)
    | lam (_) (_) s0 s1 => congr_lam ((extRen_ty xity zetaty Eqty) s0) ((extRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upExtRen_vl_ty (_) (_) Eqty) (upExtRen_vl_vl (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((extRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upExtRen_ty_ty (_) (_) Eqty) (upExtRen_ty_vl (_) (_) Eqvl)) s0)
    end.

Definition upExt_ty_vl { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) (tau : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, sigma x = tau x) : forall x, (up_ty_vl sigma) x = (up_ty_vl tau) x :=
  fun n => (ap) (ren_vl (shift) (id)) (Eq n).

Definition upExt_vl_ty { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) (tau : (fin) (m) -> ty (nty)) (Eq : forall x, sigma x = tau x) : forall x, (up_vl_ty sigma) x = (up_vl_ty tau) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition upExt_vl_vl { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) (tau : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, sigma x = tau x) : forall x, (up_vl_vl sigma) x = (up_vl_vl tau) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_vl (id) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upExt_list_ty_vl { p : nat } { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) (tau : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, sigma x = tau x) : forall x, (upList_ty_vl p sigma) x = (upList_ty_vl p tau) x :=
  fun n => (ap) (ren_vl (shift_p p) (id)) (Eq n).

Definition upExt_list_vl_ty { p : nat } { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (nty)) (tau : (fin) (m) -> ty (nty)) (Eq : forall x, sigma x = tau x) : forall x, (upList_vl_ty p sigma) x = (upList_vl_ty p tau) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition upExt_list_vl_vl { p : nat } { m : nat } { nty nvl : nat } (sigma : (fin) (m) -> vl (nty) (nvl)) (tau : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, sigma x = tau x) : forall x, (upList_vl_vl p sigma) x = (upList_vl_vl p tau) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (ren_vl (id) (shift_p p)) (Eq n)).

Fixpoint ext_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (tauty : (fin) (mty) -> ty (nty)) (tauvl : (fin) (mvl) -> vl (nty) (nvl)) (Eqty : forall x, sigmaty x = tauty x) (Eqvl : forall x, sigmavl x = tauvl x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = subst_tm tauty tauvl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl) s0) ((ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl) s0) ((ext_ty sigmaty tauty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((ext_vl sigmaty sigmavl tauty tauvl Eqty Eqvl) s0)
    end
 with ext_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (tauty : (fin) (mty) -> ty (nty)) (tauvl : (fin) (mvl) -> vl (nty) (nvl)) (Eqty : forall x, sigmaty x = tauty x) (Eqvl : forall x, sigmavl x = tauvl x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = subst_vl tauty tauvl s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((ext_ty sigmaty tauty Eqty) s0) ((ext_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (upExt_vl_ty (_) (_) Eqty) (upExt_vl_vl (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((ext_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (upExt_ty_ty (_) (_) Eqty) (upExt_ty_vl (_) (_) Eqvl)) s0)
    end.

Definition up_ren_ren_ty_vl { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_ty_vl tau) (upRen_ty_vl xi)) x = (upRen_ty_vl theta) x :=
  Eq.

Definition up_ren_ren_vl_ty { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_vl_ty tau) (upRen_vl_ty xi)) x = (upRen_vl_ty theta) x :=
  Eq.

Definition up_ren_ren_vl_vl { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_vl_vl tau) (upRen_vl_vl xi)) x = (upRen_vl_vl theta) x :=
  up_ren_ren xi tau theta Eq.

Definition up_ren_ren_list_ty_vl { p : nat } { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRenList_ty_vl p tau) (upRenList_ty_vl p xi)) x = (upRenList_ty_vl p theta) x :=
  Eq.

Definition up_ren_ren_list_vl_ty { p : nat } { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRenList_vl_ty p tau) (upRenList_vl_ty p xi)) x = (upRenList_vl_ty p theta) x :=
  Eq.

Definition up_ren_ren_list_vl_vl { p : nat } { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRenList_vl_vl p tau) (upRenList_vl_vl p xi)) x = (upRenList_vl_vl p theta) x :=
  up_ren_ren_p Eq.

Fixpoint compRenRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (rhoty : (fin) (mty) -> (fin) (lty)) (rhovl : (fin) (mvl) -> (fin) (lvl)) (Eqty : forall x, ((funcomp) zetaty xity) x = rhoty x) (Eqvl : forall x, ((funcomp) zetavl xivl) x = rhovl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm rhoty rhovl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl) s0) ((compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl) s0) ((compRenRen_ty xity zetaty rhoty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compRenRen_vl xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl) s0)
    end
 with compRenRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (rhoty : (fin) (mty) -> (fin) (lty)) (rhovl : (fin) (mvl) -> (fin) (lvl)) (Eqty : forall x, ((funcomp) zetaty xity) x = rhoty x) (Eqvl : forall x, ((funcomp) zetavl xivl) x = rhovl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl rhoty rhovl s :=
    match s with
    | var_vl (_) (_) s => (ap) (var_vl (lty) (lvl)) (Eqvl s)
    | lam (_) (_) s0 s1 => congr_lam ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upRen_vl_ty rhoty) (upRen_vl_vl rhovl) Eqty (up_ren_ren (_) (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((compRenRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upRen_ty_ty rhoty) (upRen_ty_vl rhovl) (up_ren_ren (_) (_) (_) Eqty) Eqvl) s0)
    end.

Definition up_ren_subst_ty_vl { k : nat } { l : nat } { mty mvl : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_ty_vl tau) (upRen_ty_vl xi)) x = (up_ty_vl theta) x :=
  fun n => (ap) (ren_vl (shift) (id)) (Eq n).

Definition up_ren_subst_vl_ty { k : nat } { l : nat } { mty : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_vl_ty tau) (upRen_vl_ty xi)) x = (up_vl_ty theta) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition up_ren_subst_vl_vl { k : nat } { l : nat } { mty mvl : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_vl_vl tau) (upRen_vl_vl xi)) x = (up_vl_vl theta) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_vl (id) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition up_ren_subst_list_ty_vl { p : nat } { k : nat } { l : nat } { mty mvl : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_ty_vl p tau) (upRenList_ty_vl p xi)) x = (upList_ty_vl p theta) x :=
  fun n => (ap) (ren_vl (shift_p p) (id)) (Eq n).

Definition up_ren_subst_list_vl_ty { p : nat } { k : nat } { l : nat } { mty : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_vl_ty p tau) (upRenList_vl_ty p xi)) x = (upList_vl_ty p theta) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition up_ren_subst_list_vl_vl { p : nat } { k : nat } { l : nat } { mty mvl : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_vl_vl p tau) (upRenList_vl_vl p xi)) x = (upList_vl_vl p theta) x :=
  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_vl (id) (shift_p p)) (Eq z)))).

Fixpoint compRenSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) tauty xity) x = thetaty x) (Eqvl : forall x, ((funcomp) tauvl xivl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm thetaty thetavl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl) s0) ((compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl) s0) ((compRenSubst_ty xity tauty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compRenSubst_vl xity xivl tauty tauvl thetaty thetavl Eqty Eqvl) s0)
    end
 with compRenSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) tauty xity) x = thetaty x) (Eqvl : forall x, ((funcomp) tauvl xivl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl thetaty thetavl s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_ren_subst_vl_ty (_) (_) (_) Eqty) (up_ren_subst_vl_vl (_) (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((compRenSubst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_ren_subst_ty_ty (_) (_) (_) Eqty) (up_ren_subst_ty_vl (_) (_) (_) Eqvl)) s0)
    end.

Definition up_subst_ren_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetavl : (fin) (lvl) -> (fin) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (ren_vl zetaty zetavl) sigma) x = theta x) : forall x, ((funcomp) (ren_vl (upRen_ty_ty zetaty) (upRen_ty_vl zetavl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
  fun n => (eq_trans) (compRenRen_vl (shift) (id) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) ((funcomp) (shift) zetaty) ((funcomp) (id) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_vl zetaty zetavl (shift) (id) ((funcomp) (shift) zetaty) ((funcomp) (id) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_vl (shift) (id)) (Eq n))).

Definition up_subst_ren_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (zetaty : (fin) (lty) -> (fin) (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (ren_ty zetaty) sigma) x = theta x) : forall x, ((funcomp) (ren_ty (upRen_vl_ty zetaty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
  fun n => (eq_trans) (compRenRen_ty (id) (upRen_vl_ty zetaty) ((funcomp) (id) zetaty) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_ty zetaty (id) ((funcomp) (id) zetaty) (fun x => eq_refl) (sigma n))) ((ap) (ren_ty (id)) (Eq n))).

Definition up_subst_ren_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetavl : (fin) (lvl) -> (fin) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (ren_vl zetaty zetavl) sigma) x = theta x) : forall x, ((funcomp) (ren_vl (upRen_vl_ty zetaty) (upRen_vl_vl zetavl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenRen_vl (id) (shift) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) ((funcomp) (id) zetaty) ((funcomp) (shift) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compRenRen_vl zetaty zetavl (id) (shift) ((funcomp) (id) zetaty) ((funcomp) (shift) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_vl (id) (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_ren_list_ty_vl { p : nat } { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetavl : (fin) (lvl) -> (fin) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (ren_vl zetaty zetavl) sigma) x = theta x) : forall x, ((funcomp) (ren_vl (upRenList_ty_ty p zetaty) (upRenList_ty_vl p zetavl)) (upList_ty_vl p sigma)) x = (upList_ty_vl p theta) x :=
  fun n => (eq_trans) (compRenRen_vl (shift_p p) (id) (upRenList_ty_ty p zetaty) (upRenList_ty_vl p zetavl) ((funcomp) (shift_p p) zetaty) ((funcomp) (id) zetavl) (fun x => scons_p_tail' (_) (_) x) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_vl zetaty zetavl (shift_p p) (id) ((funcomp) (shift_p p) zetaty) ((funcomp) (id) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_vl (shift_p p) (id)) (Eq n))).

Definition up_subst_ren_list_vl_ty { p : nat } { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (zetaty : (fin) (lty) -> (fin) (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (ren_ty zetaty) sigma) x = theta x) : forall x, ((funcomp) (ren_ty (upRenList_vl_ty p zetaty)) (upList_vl_ty p sigma)) x = (upList_vl_ty p theta) x :=
  fun n => (eq_trans) (compRenRen_ty (id) (upRenList_vl_ty p zetaty) ((funcomp) (id) zetaty) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_ty zetaty (id) ((funcomp) (id) zetaty) (fun x => eq_refl) (sigma n))) ((ap) (ren_ty (id)) (Eq n))).

Definition up_subst_ren_list_vl_vl { p : nat } { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetavl : (fin) (lvl) -> (fin) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (ren_vl zetaty zetavl) sigma) x = theta x) : forall x, ((funcomp) (ren_vl (upRenList_vl_ty p zetaty) (upRenList_vl_vl p zetavl)) (upList_vl_vl p sigma)) x = (upList_vl_vl p theta) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (_) n) (scons_p_congr (fun x => (ap) (var_vl (mty) (p+ mvl)) (scons_p_head' (_) (_) x)) (fun n => (eq_trans) (compRenRen_vl (id) (shift_p p) (upRenList_vl_ty p zetaty) (upRenList_vl_vl p zetavl) ((funcomp) (id) zetaty) ((funcomp) (shift_p p) zetavl) (fun x => eq_refl) (fun x => scons_p_tail' (_) (_) x) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_vl zetaty zetavl (id) (shift_p p) ((funcomp) (id) zetaty) ((funcomp) (shift_p p) zetavl) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_vl (id) (shift_p p)) (Eq n))))).

Fixpoint compSubstRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : forall x, ((funcomp) (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((compSubstRen_tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl) s0) ((compSubstRen_tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compSubstRen_tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl) s0) ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compSubstRen_vl sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl) s0)
    end
 with compSubstRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : forall x, ((funcomp) (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_ren_vl_ty (_) (_) (_) Eqty) (up_subst_ren_vl_vl (_) (_) (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((compSubstRen_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_ren_ty_ty (_) (_) (_) Eqty) (up_subst_ren_ty_vl (_) (_) (_) (_) Eqvl)) s0)
    end.

Definition up_subst_subst_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (tauty : (fin) (lty) -> ty (mty)) (tauvl : (fin) (lvl) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (subst_vl tauty tauvl) sigma) x = theta x) : forall x, ((funcomp) (subst_vl (up_ty_ty tauty) (up_ty_vl tauvl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
  fun n => (eq_trans) (compRenSubst_vl (shift) (id) (up_ty_ty tauty) (up_ty_vl tauvl) ((funcomp) (up_ty_ty tauty) (shift)) ((funcomp) (up_ty_vl tauvl) (id)) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_vl tauty tauvl (shift) (id) ((funcomp) (ren_ty (shift)) tauty) ((funcomp) (ren_vl (shift) (id)) tauvl) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_vl (shift) (id)) (Eq n))).

Definition up_subst_subst_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (tauty : (fin) (lty) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (subst_ty tauty) sigma) x = theta x) : forall x, ((funcomp) (subst_ty (up_vl_ty tauty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
  fun n => (eq_trans) (compRenSubst_ty (id) (up_vl_ty tauty) ((funcomp) (up_vl_ty tauty) (id)) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_ty tauty (id) ((funcomp) (ren_ty (id)) tauty) (fun x => eq_refl) (sigma n))) ((ap) (ren_ty (id)) (Eq n))).

Definition up_subst_subst_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (tauty : (fin) (lty) -> ty (mty)) (tauvl : (fin) (lvl) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (subst_vl tauty tauvl) sigma) x = theta x) : forall x, ((funcomp) (subst_vl (up_vl_ty tauty) (up_vl_vl tauvl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenSubst_vl (id) (shift) (up_vl_ty tauty) (up_vl_vl tauvl) ((funcomp) (up_vl_ty tauty) (id)) ((funcomp) (up_vl_vl tauvl) (shift)) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_vl tauty tauvl (id) (shift) ((funcomp) (ren_ty (id)) tauty) ((funcomp) (ren_vl (id) (shift)) tauvl) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_vl (id) (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_subst_list_ty_vl { p : nat } { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (tauty : (fin) (lty) -> ty (mty)) (tauvl : (fin) (lvl) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (subst_vl tauty tauvl) sigma) x = theta x) : forall x, ((funcomp) (subst_vl (upList_ty_ty p tauty) (upList_ty_vl p tauvl)) (upList_ty_vl p sigma)) x = (upList_ty_vl p theta) x :=
  fun n => (eq_trans) (compRenSubst_vl (shift_p p) (id) (upList_ty_ty p tauty) (upList_ty_vl p tauvl) ((funcomp) (upList_ty_ty p tauty) (shift_p p)) ((funcomp) (upList_ty_vl p tauvl) (id)) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_vl tauty tauvl (shift_p p) (id) (_) (_) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (fun x => (eq_sym) (eq_refl)) (sigma n))) ((ap) (ren_vl (shift_p p) (id)) (Eq n))).

Definition up_subst_subst_list_vl_ty { p : nat } { k : nat } { lty : nat } { mty : nat } (sigma : (fin) (k) -> ty (lty)) (tauty : (fin) (lty) -> ty (mty)) (theta : (fin) (k) -> ty (mty)) (Eq : forall x, ((funcomp) (subst_ty tauty) sigma) x = theta x) : forall x, ((funcomp) (subst_ty (upList_vl_ty p tauty)) (upList_vl_ty p sigma)) x = (upList_vl_ty p theta) x :=
  fun n => (eq_trans) (compRenSubst_ty (id) (upList_vl_ty p tauty) ((funcomp) (upList_vl_ty p tauty) (id)) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_ty tauty (id) (_) (fun x => (eq_sym) (eq_refl)) (sigma n))) ((ap) (ren_ty (id)) (Eq n))).

Definition up_subst_subst_list_vl_vl { p : nat } { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : (fin) (k) -> vl (lty) (lvl)) (tauty : (fin) (lty) -> ty (mty)) (tauvl : (fin) (lvl) -> vl (mty) (mvl)) (theta : (fin) (k) -> vl (mty) (mvl)) (Eq : forall x, ((funcomp) (subst_vl tauty tauvl) sigma) x = theta x) : forall x, ((funcomp) (subst_vl (upList_vl_ty p tauty) (upList_vl_vl p tauvl)) (upList_vl_vl p sigma)) x = (upList_vl_vl p theta) x :=
  fun n => (eq_trans) (scons_p_comp' ((funcomp) (var_vl (lty) (p+ lvl)) (zero_p p)) (_) (_) n) (scons_p_congr (fun x => scons_p_head' (_) (fun z => ren_vl (id) (shift_p p) (_)) x) (fun n => (eq_trans) (compRenSubst_vl (id) (shift_p p) (upList_vl_ty p tauty) (upList_vl_vl p tauvl) ((funcomp) (upList_vl_ty p tauty) (id)) ((funcomp) (upList_vl_vl p tauvl) (shift_p p)) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_vl tauty tauvl (id) (shift_p p) (_) (_) (fun x => (eq_sym) (eq_refl)) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (sigma n))) ((ap) (ren_vl (id) (shift_p p)) (Eq n))))).

Fixpoint compSubstSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : forall x, ((funcomp) (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl) s0) ((compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl) s0) ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compSubstSubst_vl sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl) s0)
    end
 with compSubstSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (thetaty : (fin) (mty) -> ty (lty)) (thetavl : (fin) (mvl) -> vl (lty) (lvl)) (Eqty : forall x, ((funcomp) (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : forall x, ((funcomp) (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_subst_vl_ty (_) (_) (_) Eqty) (up_subst_subst_vl_vl (_) (_) (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((compSubstSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_subst_ty_ty (_) (_) (_) Eqty) (up_subst_subst_ty_vl (_) (_) (_) (_) Eqvl)) s0)
    end.

Definition rinstInst_up_ty_vl { m : nat } { nty nvl : nat } (xi : (fin) (m) -> (fin) (nvl)) (sigma : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, ((funcomp) (var_vl (nty) (nvl)) xi) x = sigma x) : forall x, ((funcomp) (var_vl ((S) nty) (nvl)) (upRen_ty_vl xi)) x = (up_ty_vl sigma) x :=
  fun n => (ap) (ren_vl (shift) (id)) (Eq n).

Definition rinstInst_up_vl_ty { m : nat } { nty : nat } (xi : (fin) (m) -> (fin) (nty)) (sigma : (fin) (m) -> ty (nty)) (Eq : forall x, ((funcomp) (var_ty (nty)) xi) x = sigma x) : forall x, ((funcomp) (var_ty (nty)) (upRen_vl_ty xi)) x = (up_vl_ty sigma) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition rinstInst_up_vl_vl { m : nat } { nty nvl : nat } (xi : (fin) (m) -> (fin) (nvl)) (sigma : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, ((funcomp) (var_vl (nty) (nvl)) xi) x = sigma x) : forall x, ((funcomp) (var_vl (nty) ((S) nvl)) (upRen_vl_vl xi)) x = (up_vl_vl sigma) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_vl (id) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition rinstInst_up_list_ty_vl { p : nat } { m : nat } { nty nvl : nat } (xi : (fin) (m) -> (fin) (nvl)) (sigma : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, ((funcomp) (var_vl (nty) (nvl)) xi) x = sigma x) : forall x, ((funcomp) (var_vl (p+ nty) (nvl)) (upRenList_ty_vl p xi)) x = (upList_ty_vl p sigma) x :=
  fun n => (ap) (ren_vl (shift_p p) (id)) (Eq n).

Definition rinstInst_up_list_vl_ty { p : nat } { m : nat } { nty : nat } (xi : (fin) (m) -> (fin) (nty)) (sigma : (fin) (m) -> ty (nty)) (Eq : forall x, ((funcomp) (var_ty (nty)) xi) x = sigma x) : forall x, ((funcomp) (var_ty (nty)) (upRenList_vl_ty p xi)) x = (upList_vl_ty p sigma) x :=
  fun n => (ap) (ren_ty (id)) (Eq n).

Definition rinstInst_up_list_vl_vl { p : nat } { m : nat } { nty nvl : nat } (xi : (fin) (m) -> (fin) (nvl)) (sigma : (fin) (m) -> vl (nty) (nvl)) (Eq : forall x, ((funcomp) (var_vl (nty) (nvl)) xi) x = sigma x) : forall x, ((funcomp) (var_vl (nty) (p+ nvl)) (upRenList_vl_vl p xi)) x = (upList_vl_vl p sigma) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (var_vl (nty) (p+ nvl)) n) (scons_p_congr (fun z => eq_refl) (fun n => (ap) (ren_vl (id) (shift_p p)) (Eq n))).

Fixpoint rinst_inst_tm { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (Eqty : forall x, ((funcomp) (var_ty (nty)) xity) x = sigmaty x) (Eqvl : forall x, ((funcomp) (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = subst_tm sigmaty sigmavl s :=
    match s with
    | app (_) (_) s0 s1 => congr_app ((rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl) s0) ((rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl) s0) ((rinst_inst_ty xity sigmaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((rinst_inst_vl xity xivl sigmaty sigmavl Eqty Eqvl) s0)
    end
 with rinst_inst_vl { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) (Eqty : forall x, ((funcomp) (var_ty (nty)) xity) x = sigmaty x) (Eqvl : forall x, ((funcomp) (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = subst_vl sigmaty sigmavl s :=
    match s with
    | var_vl (_) (_) s => Eqvl s
    | lam (_) (_) s0 s1 => congr_lam ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty sigmaty) (up_vl_vl sigmavl) (rinstInst_up_vl_ty (_) (_) Eqty) (rinstInst_up_vl_vl (_) (_) Eqvl)) s1)
    | tlam (_) (_) s0 => congr_tlam ((rinst_inst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty sigmaty) (up_ty_vl sigmavl) (rinstInst_up_ty_ty (_) (_) Eqty) (rinstInst_up_ty_vl (_) (_) Eqvl)) s0)
    end.

Lemma rinstInst_tm { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) : ren_tm xity xivl = subst_tm ((funcomp) (var_ty (nty)) xity) ((funcomp) (var_vl (nty) (nvl)) xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_tm xity xivl (_) (_) (fun n => eq_refl) (fun n => eq_refl) x)). Qed.

Lemma rinstInst_vl { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) : ren_vl xity xivl = subst_vl ((funcomp) (var_ty (nty)) xity) ((funcomp) (var_vl (nty) (nvl)) xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_vl xity xivl (_) (_) (fun n => eq_refl) (fun n => eq_refl) x)). Qed.

Lemma instId_tm { mty mvl : nat } : subst_tm (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_tm (var_ty (mty)) (var_vl (mty) (mvl)) (fun n => eq_refl) (fun n => eq_refl) ((id) x))). Qed.

Lemma instId_vl { mty mvl : nat } : subst_vl (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_vl (var_ty (mty)) (var_vl (mty) (mvl)) (fun n => eq_refl) (fun n => eq_refl) ((id) x))). Qed.

Lemma rinstId_tm { mty mvl : nat } : @ren_tm (mty) (mvl) (mty) (mvl) (id) (id) = id .
Proof. exact ((eq_trans) (rinstInst_tm ((id) (_)) ((id) (_))) instId_tm). Qed.

Lemma rinstId_vl { mty mvl : nat } : @ren_vl (mty) (mvl) (mty) (mvl) (id) (id) = id .
Proof. exact ((eq_trans) (rinstInst_vl ((id) (_)) ((id) (_))) instId_vl). Qed.

Lemma varL_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmavl : (fin) (mvl) -> vl (nty) (nvl)) : (funcomp) (subst_vl sigmaty sigmavl) (var_vl (mty) (mvl)) = sigmavl .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma varLRen_vl { mty mvl : nat } { nty nvl : nat } (xity : (fin) (mty) -> (fin) (nty)) (xivl : (fin) (mvl) -> (fin) (nvl)) : (funcomp) (ren_vl xity xivl) (var_vl (mty) (mvl)) = (funcomp) (var_vl (nty) (nvl)) xivl .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma compComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_tm sigmaty sigmavl tauty tauvl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_vl sigmaty sigmavl tauty tauvl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) : (funcomp) (subst_tm tauty tauvl) (subst_tm sigmaty sigmavl) = subst_tm ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_vl tauty tauvl) sigmavl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmaty sigmavl tauty tauvl n)). Qed.

Lemma compComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) : (funcomp) (subst_vl tauty tauvl) (subst_vl sigmaty sigmavl) = subst_vl ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_vl tauty tauvl) sigmavl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_vl sigmaty sigmavl tauty tauvl n)). Qed.

Lemma compRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen_tm sigmaty sigmavl zetaty zetavl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen_vl sigmaty sigmavl zetaty zetavl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) : (funcomp) (ren_tm zetaty zetavl) (subst_tm sigmaty sigmavl) = subst_tm ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_vl zetaty zetavl) sigmavl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_tm sigmaty sigmavl zetaty zetavl n)). Qed.

Lemma compRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmavl : (fin) (mvl) -> vl (kty) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) : (funcomp) (ren_vl zetaty zetavl) (subst_vl sigmaty sigmavl) = subst_vl ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_vl zetaty zetavl) sigmavl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_vl sigmaty sigmavl zetaty zetavl n)). Qed.

Lemma renComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm ((funcomp) tauty xity) ((funcomp) tauvl xivl) s .
Proof. exact (compRenSubst_tm xity xivl tauty tauvl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl ((funcomp) tauty xity) ((funcomp) tauvl xivl) s .
Proof. exact (compRenSubst_vl xity xivl tauty tauvl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) : (funcomp) (subst_tm tauty tauvl) (ren_tm xity xivl) = subst_tm ((funcomp) tauty xity) ((funcomp) tauvl xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_tm xity xivl tauty tauvl n)). Qed.

Lemma renComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (tauty : (fin) (kty) -> ty (lty)) (tauvl : (fin) (kvl) -> vl (lty) (lvl)) : (funcomp) (subst_vl tauty tauvl) (ren_vl xity xivl) = subst_vl ((funcomp) tauty xity) ((funcomp) tauvl xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_vl xity xivl tauty tauvl n)). Qed.

Lemma renRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm ((funcomp) zetaty xity) ((funcomp) zetavl xivl) s .
Proof. exact (compRenRen_tm xity xivl zetaty zetavl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl ((funcomp) zetaty xity) ((funcomp) zetavl xivl) s .
Proof. exact (compRenRen_vl xity xivl zetaty zetavl (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) : (funcomp) (ren_tm zetaty zetavl) (ren_tm xity xivl) = ren_tm ((funcomp) zetaty xity) ((funcomp) zetavl xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_tm xity xivl zetaty zetavl n)). Qed.

Lemma renRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : (fin) (mty) -> (fin) (kty)) (xivl : (fin) (mvl) -> (fin) (kvl)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetavl : (fin) (kvl) -> (fin) (lvl)) : (funcomp) (ren_vl zetaty zetavl) (ren_vl xity xivl) = ren_vl ((funcomp) zetaty xity) ((funcomp) zetavl xivl) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_vl xity xivl zetaty zetavl n)). Qed.

End tmvl.

Arguments var_ty {nty}.

Arguments arr {nty}.

Arguments all {nty}.

Arguments app {nty} {nvl}.

Arguments tapp {nty} {nvl}.

Arguments vt {nty} {nvl}.

Arguments var_vl {nty} {nvl}.

Arguments lam {nty} {nvl}.

Arguments tlam {nty} {nvl}.

Global Instance Subst_ty { mty : nat } { nty : nat } : Subst1 ((fin) (mty) -> ty (nty)) (ty (mty)) (ty (nty)) := @subst_ty (mty) (nty) .

Global Instance Subst_tm { mty mvl : nat } { nty nvl : nat } : Subst2 ((fin) (mty) -> ty (nty)) ((fin) (mvl) -> vl (nty) (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @subst_tm (mty) (mvl) (nty) (nvl) .

Global Instance Subst_vl { mty mvl : nat } { nty nvl : nat } : Subst2 ((fin) (mty) -> ty (nty)) ((fin) (mvl) -> vl (nty) (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @subst_vl (mty) (mvl) (nty) (nvl) .

Global Instance Ren_ty { mty : nat } { nty : nat } : Ren1 ((fin) (mty) -> (fin) (nty)) (ty (mty)) (ty (nty)) := @ren_ty (mty) (nty) .

Global Instance Ren_tm { mty mvl : nat } { nty nvl : nat } : Ren2 ((fin) (mty) -> (fin) (nty)) ((fin) (mvl) -> (fin) (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @ren_tm (mty) (mvl) (nty) (nvl) .

Global Instance Ren_vl { mty mvl : nat } { nty nvl : nat } : Ren2 ((fin) (mty) -> (fin) (nty)) ((fin) (mvl) -> (fin) (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @ren_vl (mty) (mvl) (nty) (nvl) .

Global Instance VarInstance_ty { mty : nat } : Var ((fin) (mty)) (ty (mty)) := @var_ty (mty) .

Notation "x '__ty'" := (var_ty x) (at level 5, format "x __ty") : subst_scope.

Notation "x '__ty'" := (@ids (_) (_) VarInstance_ty x) (at level 5, only printing, format "x __ty") : subst_scope.

Notation "'var'" := (var_ty) (only printing, at level 1) : subst_scope.

Global Instance VarInstance_vl { mty mvl : nat } : Var ((fin) (mvl)) (vl (mty) (mvl)) := @var_vl (mty) (mvl) .

Notation "x '__vl'" := (var_vl x) (at level 5, format "x __vl") : subst_scope.

Notation "x '__vl'" := (@ids (_) (_) VarInstance_vl x) (at level 5, only printing, format "x __vl") : subst_scope.

Notation "'var'" := (var_vl) (only printing, at level 1) : subst_scope.

Class Up_ty X Y := up_ty : X -> Y.

Notation "↑__ty" := (up_ty) (only printing) : subst_scope.

Class Up_vl X Y := up_vl : X -> Y.

Notation "↑__vl" := (up_vl) (only printing) : subst_scope.

Notation "↑__ty" := (up_ty_ty) (only printing) : subst_scope.

Global Instance Up_ty_ty { m : nat } { nty : nat } : Up_ty (_) (_) := @up_ty_ty (m) (nty) .

Notation "↑__ty" := (up_ty_vl) (only printing) : subst_scope.

Global Instance Up_ty_vl { m : nat } { nty nvl : nat } : Up_vl (_) (_) := @up_ty_vl (m) (nty) (nvl) .

Notation "↑__vl" := (up_vl_ty) (only printing) : subst_scope.

Global Instance Up_vl_ty { m : nat } { nty : nat } : Up_ty (_) (_) := @up_vl_ty (m) (nty) .

Notation "↑__vl" := (up_vl_vl) (only printing) : subst_scope.

Global Instance Up_vl_vl { m : nat } { nty nvl : nat } : Up_vl (_) (_) := @up_vl_vl (m) (nty) (nvl) .

Notation "s [ sigmaty ]" := (subst_ty sigmaty s) (at level 7, left associativity, only printing) : subst_scope.

Notation "[ sigmaty ]" := (subst_ty sigmaty) (at level 1, left associativity, only printing) : fscope.

Notation "s ⟨ xity ⟩" := (ren_ty xity s) (at level 7, left associativity, only printing) : subst_scope.

Notation "⟨ xity ⟩" := (ren_ty xity) (at level 1, left associativity, only printing) : fscope.

Notation "s [ sigmaty ; sigmavl ]" := (subst_tm sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.

Notation "[ sigmaty ; sigmavl ]" := (subst_tm sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.

Notation "s ⟨ xity ; xivl ⟩" := (ren_tm xity xivl s) (at level 7, left associativity, only printing) : subst_scope.

Notation "⟨ xity ; xivl ⟩" := (ren_tm xity xivl) (at level 1, left associativity, only printing) : fscope.

Notation "s [ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.

Notation "[ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.

Notation "s ⟨ xity ; xivl ⟩" := (ren_vl xity xivl s) (at level 7, left associativity, only printing) : subst_scope.

Notation "⟨ xity ; xivl ⟩" := (ren_vl xity xivl) (at level 1, left associativity, only printing) : fscope.

Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_ty, Subst_tm, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl.

Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_ty, Subst_tm, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl in *.

Ltac asimpl' := repeat first [progress rewrite ?instId_ty| progress rewrite ?compComp_ty| progress rewrite ?compComp'_ty| progress rewrite ?instId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_tm| progress rewrite ?instId_vl| progress rewrite ?compComp_vl| progress rewrite ?compComp'_vl| progress rewrite ?rinstId_ty| progress rewrite ?compRen_ty| progress rewrite ?compRen'_ty| progress rewrite ?renComp_ty| progress rewrite ?renComp'_ty| progress rewrite ?renRen_ty| progress rewrite ?renRen'_ty| progress rewrite ?rinstId_tm| progress rewrite ?compRen_tm| progress rewrite ?compRen'_tm| progress rewrite ?renComp_tm| progress rewrite ?renComp'_tm| progress rewrite ?renRen_tm| progress rewrite ?renRen'_tm| progress rewrite ?rinstId_vl| progress rewrite ?compRen_vl| progress rewrite ?compRen'_vl| progress rewrite ?renComp_vl| progress rewrite ?renComp'_vl| progress rewrite ?renRen_vl| progress rewrite ?renRen'_vl| progress rewrite ?varL_ty| progress rewrite ?varL_vl| progress rewrite ?varLRen_ty| progress rewrite ?varLRen_vl| progress (unfold up_ren, upRen_ty_ty, upRenList_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, upRenList_ty_vl, upRenList_vl_ty, upRenList_vl_vl, up_ty_ty, upList_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl, upList_ty_vl, upList_vl_ty, upList_vl_vl)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl])| fsimpl].

Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.

Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.

Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).

Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_ty in *| progress rewrite ?compComp_ty in *| progress rewrite ?compComp'_ty in *| progress rewrite ?instId_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_tm in *| progress rewrite ?instId_vl in *| progress rewrite ?compComp_vl in *| progress rewrite ?compComp'_vl in *| progress rewrite ?rinstId_ty in *| progress rewrite ?compRen_ty in *| progress rewrite ?compRen'_ty in *| progress rewrite ?renComp_ty in *| progress rewrite ?renComp'_ty in *| progress rewrite ?renRen_ty in *| progress rewrite ?renRen'_ty in *| progress rewrite ?rinstId_tm in *| progress rewrite ?compRen_tm in *| progress rewrite ?compRen'_tm in *| progress rewrite ?renComp_tm in *| progress rewrite ?renComp'_tm in *| progress rewrite ?renRen_tm in *| progress rewrite ?renRen'_tm in *| progress rewrite ?rinstId_vl in *| progress rewrite ?compRen_vl in *| progress rewrite ?compRen'_vl in *| progress rewrite ?renComp_vl in *| progress rewrite ?renComp'_vl in *| progress rewrite ?renRen_vl in *| progress rewrite ?renRen'_vl in *| progress rewrite ?varL_ty in *| progress rewrite ?varL_vl in *| progress rewrite ?varLRen_ty in *| progress rewrite ?varLRen_vl in *| progress (unfold up_ren, upRen_ty_ty, upRenList_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, upRenList_ty_vl, upRenList_vl_ty, upRenList_vl_vl, up_ty_ty, upList_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl, upList_ty_vl, upList_vl_ty, upList_vl_vl in *)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl] in *)| fsimpl in *].

Ltac substify := auto_unfold; try repeat (erewrite rinstInst_ty); try repeat (erewrite rinstInst_tm); try repeat (erewrite rinstInst_vl).

Ltac renamify := auto_unfold; try repeat (erewrite <- rinstInst_ty); try repeat (erewrite <- rinstInst_tm); try repeat (erewrite <- rinstInst_vl).