Require Export fintype.

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

Definition congr_top { mty : nat } : top (mty) = top (mty) :=
  eq_refl.

Definition 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 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => arr (mty) x (_)) H1)) ((ap) (fun x => arr (mty) (_) x) H2).

Definition congr_all { mty : nat } { s0 : ty (mty) } { s1 : ty ((S) mty) } { t0 : ty (mty) } { t1 : ty ((S) mty) } (H1 : s0 = t0) (H2 : s1 = t1) : all (mty) s0 s1 = all (mty) t0 t1 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => all (mty) x (_)) H1)) ((ap) (fun x => all (mty) (_) x) H2).

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

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

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

Definition up_ty_ty { m : nat } { nty : nat } (sigma : (fin) (m) -> ty (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)) : _ :=
  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)) : _ :=
    match s with
    | var_ty (_) s => sigmaty s
    | top (_) => top (nty)
    | arr (_) s0 s1 => arr (nty) ((subst_ty sigmaty) s0) ((subst_ty sigmaty) s1)
    | all (_) s0 s1 => all (nty) ((subst_ty sigmaty) s0) ((subst_ty (up_ty_ty sigmaty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((idSubst_ty sigmaty Eqty) s0) ((idSubst_ty sigmaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((idSubst_ty sigmaty Eqty) s0) ((idSubst_ty (up_ty_ty sigmaty) (upId_ty_ty (_) Eqty)) s1)
    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)
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((extRen_ty xity zetaty Eqty) s0) ((extRen_ty xity zetaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((extRen_ty xity zetaty Eqty) s0) ((extRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upExtRen_ty_ty (_) (_) Eqty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((ext_ty sigmaty tauty Eqty) s0) ((ext_ty sigmaty tauty Eqty) s1)
    | all (_) s0 s1 => congr_all ((ext_ty sigmaty tauty Eqty) s0) ((ext_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (upExt_ty_ty (_) (_) Eqty)) s1)
    end.

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)
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_ty xity zetaty rhoty Eqty) s1)
    | all (_) s0 s1 => congr_all ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upRen_ty_ty rhoty) (up_ren_ren (_) (_) (_) Eqty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_ty xity tauty thetaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_ty (upRen_ty_ty xity) (up_ty_ty tauty) (up_ty_ty thetaty) (up_ren_subst_ty_ty (_) (_) (_) Eqty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_ty (up_ty_ty sigmaty) (upRen_ty_ty zetaty) (up_ty_ty thetaty) (up_subst_ren_ty_ty (_) (_) (_) Eqty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (up_ty_ty thetaty) (up_subst_subst_ty_ty (_) (_) (_) Eqty)) s1)
    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
    | top (_) => congr_top
    | arr (_) s0 s1 => congr_arr ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_ty xity sigmaty Eqty) s1)
    | all (_) s0 s1 => congr_all ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_ty (upRen_ty_ty xity) (up_ty_ty sigmaty) (rinstInst_up_ty_ty (_) (_) Eqty)) s1)
    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) (ty (mty)) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_ty (var_ty (mty)) (fun n => eq_refl) (((@id) (ty (mty))) x))). Qed.

Lemma rinstId_ty { mty : nat } : ren_ty ((@id) (_)) = (@id) (ty (mty)) .
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.

Inductive tm (nty ntm : nat) : Type :=
  | var_tm : (fin) (ntm) -> tm (nty) (ntm)
  | app : tm (nty) (ntm) -> tm (nty) (ntm) -> tm (nty) (ntm)
  | tapp : tm (nty) (ntm) -> ty (nty) -> tm (nty) (ntm)
  | vt : tm (nty) (ntm) -> tm (nty) (ntm)
  | abs : ty (nty) -> tm (nty) ((S) ntm) -> tm (nty) (ntm)
  | tabs : ty (nty) -> tm ((S) nty) (ntm) -> tm (nty) (ntm).

Definition congr_app { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } { t1 : tm (mty) (mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : app (mty) (mtm) s0 s1 = app (mty) (mtm) t0 t1 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => app (mty) (mtm) x (_)) H1)) ((ap) (fun x => app (mty) (mtm) (_) x) H2).

Definition congr_tapp { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : ty (mty) } { t0 : tm (mty) (mtm) } { t1 : ty (mty) } (H1 : s0 = t0) (H2 : s1 = t1) : tapp (mty) (mtm) s0 s1 = tapp (mty) (mtm) t0 t1 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => tapp (mty) (mtm) x (_)) H1)) ((ap) (fun x => tapp (mty) (mtm) (_) x) H2).

Definition congr_vt { mty mtm : nat } { s0 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } (H1 : s0 = t0) : vt (mty) (mtm) s0 = vt (mty) (mtm) t0 :=
  (eq_trans) (eq_refl) ((ap) (fun x => vt (mty) (mtm) x) H1).

Definition congr_abs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm (mty) ((S) mtm) } { t0 : ty (mty) } { t1 : tm (mty) ((S) mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : abs (mty) (mtm) s0 s1 = abs (mty) (mtm) t0 t1 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => abs (mty) (mtm) x (_)) H1)) ((ap) (fun x => abs (mty) (mtm) (_) x) H2).

Definition congr_tabs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm ((S) mty) (mtm) } { t0 : ty (mty) } { t1 : tm ((S) mty) (mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : tabs (mty) (mtm) s0 s1 = tabs (mty) (mtm) t0 t1 :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) (fun x => tabs (mty) (mtm) x (_)) H1)) ((ap) (fun x => tabs (mty) (mtm) (_) x) H2).

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

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

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

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

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

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

Fixpoint ren_tm { mty mtm : nat } { nty ntm : nat } (xity : (fin) (mty) -> (fin) (nty)) (xitm : (fin) (mtm) -> (fin) (ntm)) (s : tm (mty) (mtm)) : _ :=
    match s with
    | var_tm (_) (_) s => (var_tm (nty) (ntm)) (xitm s)
    | app (_) (_) s0 s1 => app (nty) (ntm) ((ren_tm xity xitm) s0) ((ren_tm xity xitm) s1)
    | tapp (_) (_) s0 s1 => tapp (nty) (ntm) ((ren_tm xity xitm) s0) ((ren_ty xity) s1)
    | vt (_) (_) s0 => vt (nty) (ntm) ((ren_tm xity xitm) s0)
    | abs (_) (_) s0 s1 => abs (nty) (ntm) ((ren_ty xity) s0) ((ren_tm (upRen_tm_ty xity) (upRen_tm_tm xitm)) s1)
    | tabs (_) (_) s0 s1 => tabs (nty) (ntm) ((ren_ty xity) s0) ((ren_tm (upRen_ty_ty xity) (upRen_ty_tm xitm)) s1)
    end.

Definition up_ty_tm { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) : _ :=
  (funcomp) (ren_tm (shift) ((@id) (_))) sigma.

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

Definition up_tm_tm { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) : _ :=
  (scons) ((var_tm (nty) ((S) ntm)) (var_zero)) ((funcomp) (ren_tm ((@id) (_)) (shift)) sigma).

Definition upList_ty_tm (p : nat) { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) : _ :=
  (funcomp) (ren_tm (shift_p p) ((@id) (_))) sigma.

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

Definition upList_tm_tm (p : nat) { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) : _ :=
  scons_p p ((funcomp) (var_tm (nty) (p+ ntm)) (zero_p p)) ((funcomp) (ren_tm ((@id) (_)) (shift_p p)) sigma).

Fixpoint subst_tm { mty mtm : nat } { nty ntm : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmatm : (fin) (mtm) -> tm (nty) (ntm)) (s : tm (mty) (mtm)) : _ :=
    match s with
    | var_tm (_) (_) s => sigmatm s
    | app (_) (_) s0 s1 => app (nty) (ntm) ((subst_tm sigmaty sigmatm) s0) ((subst_tm sigmaty sigmatm) s1)
    | tapp (_) (_) s0 s1 => tapp (nty) (ntm) ((subst_tm sigmaty sigmatm) s0) ((subst_ty sigmaty) s1)
    | vt (_) (_) s0 => vt (nty) (ntm) ((subst_tm sigmaty sigmatm) s0)
    | abs (_) (_) s0 s1 => abs (nty) (ntm) ((subst_ty sigmaty) s0) ((subst_tm (up_tm_ty sigmaty) (up_tm_tm sigmatm)) s1)
    | tabs (_) (_) s0 s1 => tabs (nty) (ntm) ((subst_ty sigmaty) s0) ((subst_tm (up_ty_ty sigmaty) (up_ty_tm sigmatm)) s1)
    end.

Definition upId_ty_tm { mty mtm : nat } (sigma : (fin) (mtm) -> tm (mty) (mtm)) (Eq : forall x, sigma x = (var_tm (mty) (mtm)) x) : forall x, (up_ty_tm sigma) x = (var_tm ((S) mty) (mtm)) x :=
  fun n => (ap) (ren_tm (shift) ((@id) (_))) (Eq n).

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

Definition upId_tm_tm { mty mtm : nat } (sigma : (fin) (mtm) -> tm (mty) (mtm)) (Eq : forall x, sigma x = (var_tm (mty) (mtm)) x) : forall x, (up_tm_tm sigma) x = (var_tm (mty) ((S) mtm)) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upIdList_ty_tm { p : nat } { mty mtm : nat } (sigma : (fin) (mtm) -> tm (mty) (mtm)) (Eq : forall x, sigma x = (var_tm (mty) (mtm)) x) : forall x, (upList_ty_tm p sigma) x = (var_tm (p+ mty) (mtm)) x :=
  fun n => (ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n).

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

Definition upIdList_tm_tm { p : nat } { mty mtm : nat } (sigma : (fin) (mtm) -> tm (mty) (mtm)) (Eq : forall x, sigma x = (var_tm (mty) (mtm)) x) : forall x, (upList_tm_tm p sigma) x = (var_tm (mty) (p+ mtm)) x :=
  fun n => scons_p_eta (var_tm (mty) (p+ mtm)) (fun n => (ap) (ren_tm ((@id) (_)) (shift_p p)) (Eq n)) (fun n => eq_refl).

Fixpoint idSubst_tm { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (mty)) (sigmatm : (fin) (mtm) -> tm (mty) (mtm)) (Eqty : forall x, sigmaty x = (var_ty (mty)) x) (Eqtm : forall x, sigmatm x = (var_tm (mty) (mtm)) x) (s : tm (mty) (mtm)) : subst_tm sigmaty sigmatm s = s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((idSubst_tm sigmaty sigmatm Eqty Eqtm) s0) ((idSubst_tm sigmaty sigmatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((idSubst_tm sigmaty sigmatm Eqty Eqtm) s0) ((idSubst_ty sigmaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((idSubst_tm sigmaty sigmatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((idSubst_ty sigmaty Eqty) s0) ((idSubst_tm (up_tm_ty sigmaty) (up_tm_tm sigmatm) (upId_tm_ty (_) Eqty) (upId_tm_tm (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((idSubst_ty sigmaty Eqty) s0) ((idSubst_tm (up_ty_ty sigmaty) (up_ty_tm sigmatm) (upId_ty_ty (_) Eqty) (upId_ty_tm (_) Eqtm)) s1)
    end.

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

Definition upExtRen_tm_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_tm_ty xi) x = (upRen_tm_ty zeta) x :=
  fun n => Eq n.

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

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

Definition upExtRen_list_tm_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_tm_ty p xi) x = (upRenList_tm_ty p zeta) x :=
  fun n => Eq n.

Definition upExtRen_list_tm_tm { p : nat } { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRenList_tm_tm p xi) x = (upRenList_tm_tm p zeta) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (shift_p p) (Eq n)).

Fixpoint extRen_tm { mty mtm : nat } { nty ntm : nat } (xity : (fin) (mty) -> (fin) (nty)) (xitm : (fin) (mtm) -> (fin) (ntm)) (zetaty : (fin) (mty) -> (fin) (nty)) (zetatm : (fin) (mtm) -> (fin) (ntm)) (Eqty : forall x, xity x = zetaty x) (Eqtm : forall x, xitm x = zetatm x) (s : tm (mty) (mtm)) : ren_tm xity xitm s = ren_tm zetaty zetatm s :=
    match s with
    | var_tm (_) (_) s => (ap) (var_tm (nty) (ntm)) (Eqtm s)
    | app (_) (_) s0 s1 => congr_app ((extRen_tm xity xitm zetaty zetatm Eqty Eqtm) s0) ((extRen_tm xity xitm zetaty zetatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((extRen_tm xity xitm zetaty zetatm Eqty Eqtm) s0) ((extRen_ty xity zetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((extRen_tm xity xitm zetaty zetatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((extRen_ty xity zetaty Eqty) s0) ((extRen_tm (upRen_tm_ty xity) (upRen_tm_tm xitm) (upRen_tm_ty zetaty) (upRen_tm_tm zetatm) (upExtRen_tm_ty (_) (_) Eqty) (upExtRen_tm_tm (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((extRen_ty xity zetaty Eqty) s0) ((extRen_tm (upRen_ty_ty xity) (upRen_ty_tm xitm) (upRen_ty_ty zetaty) (upRen_ty_tm zetatm) (upExtRen_ty_ty (_) (_) Eqty) (upExtRen_ty_tm (_) (_) Eqtm)) s1)
    end.

Definition upExt_ty_tm { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) (tau : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (up_ty_tm sigma) x = (up_ty_tm tau) x :=
  fun n => (ap) (ren_tm (shift) ((@id) (_))) (Eq n).

Definition upExt_tm_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_tm_ty sigma) x = (up_tm_ty tau) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition upExt_tm_tm { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) (tau : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (up_tm_tm sigma) x = (up_tm_tm tau) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition upExt_list_ty_tm { p : nat } { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) (tau : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (upList_ty_tm p sigma) x = (upList_ty_tm p tau) x :=
  fun n => (ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n).

Definition upExt_list_tm_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_tm_ty p sigma) x = (upList_tm_ty p tau) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition upExt_list_tm_tm { p : nat } { m : nat } { nty ntm : nat } (sigma : (fin) (m) -> tm (nty) (ntm)) (tau : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (upList_tm_tm p sigma) x = (upList_tm_tm p tau) x :=
  fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (ren_tm ((@id) (_)) (shift_p p)) (Eq n)).

Fixpoint ext_tm { mty mtm : nat } { nty ntm : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmatm : (fin) (mtm) -> tm (nty) (ntm)) (tauty : (fin) (mty) -> ty (nty)) (tautm : (fin) (mtm) -> tm (nty) (ntm)) (Eqty : forall x, sigmaty x = tauty x) (Eqtm : forall x, sigmatm x = tautm x) (s : tm (mty) (mtm)) : subst_tm sigmaty sigmatm s = subst_tm tauty tautm s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((ext_tm sigmaty sigmatm tauty tautm Eqty Eqtm) s0) ((ext_tm sigmaty sigmatm tauty tautm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((ext_tm sigmaty sigmatm tauty tautm Eqty Eqtm) s0) ((ext_ty sigmaty tauty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((ext_tm sigmaty sigmatm tauty tautm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((ext_ty sigmaty tauty Eqty) s0) ((ext_tm (up_tm_ty sigmaty) (up_tm_tm sigmatm) (up_tm_ty tauty) (up_tm_tm tautm) (upExt_tm_ty (_) (_) Eqty) (upExt_tm_tm (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((ext_ty sigmaty tauty Eqty) s0) ((ext_tm (up_ty_ty sigmaty) (up_ty_tm sigmatm) (up_ty_ty tauty) (up_ty_tm tautm) (upExt_ty_ty (_) (_) Eqty) (upExt_ty_tm (_) (_) Eqtm)) s1)
    end.

Fixpoint compRenRen_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (rhoty : (fin) (mty) -> (fin) (lty)) (rhotm : (fin) (mtm) -> (fin) (ltm)) (Eqty : forall x, ((funcomp) zetaty xity) x = rhoty x) (Eqtm : forall x, ((funcomp) zetatm xitm) x = rhotm x) (s : tm (mty) (mtm)) : ren_tm zetaty zetatm (ren_tm xity xitm s) = ren_tm rhoty rhotm s :=
    match s with
    | var_tm (_) (_) s => (ap) (var_tm (lty) (ltm)) (Eqtm s)
    | app (_) (_) s0 s1 => congr_app ((compRenRen_tm xity xitm zetaty zetatm rhoty rhotm Eqty Eqtm) s0) ((compRenRen_tm xity xitm zetaty zetatm rhoty rhotm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compRenRen_tm xity xitm zetaty zetatm rhoty rhotm Eqty Eqtm) s0) ((compRenRen_ty xity zetaty rhoty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compRenRen_tm xity xitm zetaty zetatm rhoty rhotm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_tm (upRen_tm_ty xity) (upRen_tm_tm xitm) (upRen_tm_ty zetaty) (upRen_tm_tm zetatm) (upRen_tm_ty rhoty) (upRen_tm_tm rhotm) Eqty (up_ren_ren (_) (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((compRenRen_ty xity zetaty rhoty Eqty) s0) ((compRenRen_tm (upRen_ty_ty xity) (upRen_ty_tm xitm) (upRen_ty_ty zetaty) (upRen_ty_tm zetatm) (upRen_ty_ty rhoty) (upRen_ty_tm rhotm) (up_ren_ren (_) (_) (_) Eqty) Eqtm) s1)
    end.

Definition up_ren_subst_ty_tm { k : nat } { l : nat } { mty mtm : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_ty_tm tau) (upRen_ty_tm xi)) x = (up_ty_tm theta) x :=
  fun n => (ap) (ren_tm (shift) ((@id) (_))) (Eq n).

Definition up_ren_subst_tm_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_tm_ty tau) (upRen_tm_ty xi)) x = (up_tm_ty theta) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition up_ren_subst_tm_tm { k : nat } { l : nat } { mty mtm : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_tm_tm tau) (upRen_tm_tm xi)) x = (up_tm_tm theta) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition up_ren_subst_list_ty_tm { p : nat } { k : nat } { l : nat } { mty mtm : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_ty_tm p tau) (upRenList_ty_tm p xi)) x = (upList_ty_tm p theta) x :=
  fun n => (ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n).

Definition up_ren_subst_list_tm_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_tm_ty p tau) (upRenList_tm_ty p xi)) x = (upList_tm_ty p theta) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition up_ren_subst_list_tm_tm { p : nat } { k : nat } { l : nat } { mty mtm : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upList_tm_tm p tau) (upRenList_tm_tm p xi)) x = (upList_tm_tm 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_tm ((@id) (_)) (shift_p p)) (Eq z)))).

Fixpoint compRenSubst_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) (thetaty : (fin) (mty) -> ty (lty)) (thetatm : (fin) (mtm) -> tm (lty) (ltm)) (Eqty : forall x, ((funcomp) tauty xity) x = thetaty x) (Eqtm : forall x, ((funcomp) tautm xitm) x = thetatm x) (s : tm (mty) (mtm)) : subst_tm tauty tautm (ren_tm xity xitm s) = subst_tm thetaty thetatm s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((compRenSubst_tm xity xitm tauty tautm thetaty thetatm Eqty Eqtm) s0) ((compRenSubst_tm xity xitm tauty tautm thetaty thetatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compRenSubst_tm xity xitm tauty tautm thetaty thetatm Eqty Eqtm) s0) ((compRenSubst_ty xity tauty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compRenSubst_tm xity xitm tauty tautm thetaty thetatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_tm (upRen_tm_ty xity) (upRen_tm_tm xitm) (up_tm_ty tauty) (up_tm_tm tautm) (up_tm_ty thetaty) (up_tm_tm thetatm) (up_ren_subst_tm_ty (_) (_) (_) Eqty) (up_ren_subst_tm_tm (_) (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((compRenSubst_ty xity tauty thetaty Eqty) s0) ((compRenSubst_tm (upRen_ty_ty xity) (upRen_ty_tm xitm) (up_ty_ty tauty) (up_ty_tm tautm) (up_ty_ty thetaty) (up_ty_tm thetatm) (up_ren_subst_ty_ty (_) (_) (_) Eqty) (up_ren_subst_ty_tm (_) (_) (_) Eqtm)) s1)
    end.

Definition up_subst_ren_ty_tm { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetatm : (fin) (ltm) -> (fin) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (ren_tm zetaty zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRen_ty_ty zetaty) (upRen_ty_tm zetatm)) (up_ty_tm sigma)) x = (up_ty_tm theta) x :=
  fun n => (eq_trans) (compRenRen_tm (shift) ((@id) (_)) (upRen_ty_ty zetaty) (upRen_ty_tm zetatm) ((funcomp) (shift) zetaty) ((funcomp) ((@id) (_)) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetaty zetatm (shift) ((@id) (_)) ((funcomp) (shift) zetaty) ((funcomp) ((@id) (_)) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_tm (shift) ((@id) (_))) (Eq n))).

Definition up_subst_ren_tm_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_tm_ty zetaty)) (up_tm_ty sigma)) x = (up_tm_ty theta) x :=
  fun n => (eq_trans) (compRenRen_ty ((@id) (_)) (upRen_tm_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_tm_tm { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetatm : (fin) (ltm) -> (fin) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (ren_tm zetaty zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRen_tm_ty zetaty) (upRen_tm_tm zetatm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenRen_tm ((@id) (_)) (shift) (upRen_tm_ty zetaty) (upRen_tm_tm zetatm) ((funcomp) ((@id) (_)) zetaty) ((funcomp) (shift) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetaty zetatm ((@id) (_)) (shift) ((funcomp) ((@id) (_)) zetaty) ((funcomp) (shift) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_ren_list_ty_tm { p : nat } { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetatm : (fin) (ltm) -> (fin) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (ren_tm zetaty zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRenList_ty_ty p zetaty) (upRenList_ty_tm p zetatm)) (upList_ty_tm p sigma)) x = (upList_ty_tm p theta) x :=
  fun n => (eq_trans) (compRenRen_tm (shift_p p) ((@id) (_)) (upRenList_ty_ty p zetaty) (upRenList_ty_tm p zetatm) ((funcomp) (shift_p p) zetaty) ((funcomp) ((@id) (_)) zetatm) (fun x => scons_p_tail' (_) (_) x) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetaty zetatm (shift_p p) ((@id) (_)) ((funcomp) (shift_p p) zetaty) ((funcomp) ((@id) (_)) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n))).

Definition up_subst_ren_list_tm_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_tm_ty p zetaty)) (upList_tm_ty p sigma)) x = (upList_tm_ty p theta) x :=
  fun n => (eq_trans) (compRenRen_ty ((@id) (_)) (upRenList_tm_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_tm_tm { p : nat } { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (zetaty : (fin) (lty) -> (fin) (mty)) (zetatm : (fin) (ltm) -> (fin) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (ren_tm zetaty zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRenList_tm_ty p zetaty) (upRenList_tm_tm p zetatm)) (upList_tm_tm p sigma)) x = (upList_tm_tm p theta) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (_) n) (scons_p_congr (fun x => (ap) (var_tm (mty) (p+ mtm)) (scons_p_head' (_) (_) x)) (fun n => (eq_trans) (compRenRen_tm ((@id) (_)) (shift_p p) (upRenList_tm_ty p zetaty) (upRenList_tm_tm p zetatm) ((funcomp) ((@id) (_)) zetaty) ((funcomp) (shift_p p) zetatm) (fun x => eq_refl) (fun x => scons_p_tail' (_) (_) x) (sigma n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetaty zetatm ((@id) (_)) (shift_p p) ((funcomp) ((@id) (_)) zetaty) ((funcomp) (shift_p p) zetatm) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_tm ((@id) (_)) (shift_p p)) (Eq n))))).

Fixpoint compSubstRen_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (thetaty : (fin) (mty) -> ty (lty)) (thetatm : (fin) (mtm) -> tm (lty) (ltm)) (Eqty : forall x, ((funcomp) (ren_ty zetaty) sigmaty) x = thetaty x) (Eqtm : forall x, ((funcomp) (ren_tm zetaty zetatm) sigmatm) x = thetatm x) (s : tm (mty) (mtm)) : ren_tm zetaty zetatm (subst_tm sigmaty sigmatm s) = subst_tm thetaty thetatm s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((compSubstRen_tm sigmaty sigmatm zetaty zetatm thetaty thetatm Eqty Eqtm) s0) ((compSubstRen_tm sigmaty sigmatm zetaty zetatm thetaty thetatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compSubstRen_tm sigmaty sigmatm zetaty zetatm thetaty thetatm Eqty Eqtm) s0) ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compSubstRen_tm sigmaty sigmatm zetaty zetatm thetaty thetatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_tm (up_tm_ty sigmaty) (up_tm_tm sigmatm) (upRen_tm_ty zetaty) (upRen_tm_tm zetatm) (up_tm_ty thetaty) (up_tm_tm thetatm) (up_subst_ren_tm_ty (_) (_) (_) Eqty) (up_subst_ren_tm_tm (_) (_) (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((compSubstRen_ty sigmaty zetaty thetaty Eqty) s0) ((compSubstRen_tm (up_ty_ty sigmaty) (up_ty_tm sigmatm) (upRen_ty_ty zetaty) (upRen_ty_tm zetatm) (up_ty_ty thetaty) (up_ty_tm thetatm) (up_subst_ren_ty_ty (_) (_) (_) Eqty) (up_subst_ren_ty_tm (_) (_) (_) (_) Eqtm)) s1)
    end.

Definition up_subst_subst_ty_tm { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (tauty : (fin) (lty) -> ty (mty)) (tautm : (fin) (ltm) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (subst_tm tauty tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_ty_ty tauty) (up_ty_tm tautm)) (up_ty_tm sigma)) x = (up_ty_tm theta) x :=
  fun n => (eq_trans) (compRenSubst_tm (shift) ((@id) (_)) (up_ty_ty tauty) (up_ty_tm tautm) ((funcomp) (up_ty_ty tauty) (shift)) ((funcomp) (up_ty_tm tautm) ((@id) (_))) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tauty tautm (shift) ((@id) (_)) ((funcomp) (ren_ty (shift)) tauty) ((funcomp) (ren_tm (shift) ((@id) (_))) tautm) (fun x => eq_refl) (fun x => eq_refl) (sigma n))) ((ap) (ren_tm (shift) ((@id) (_))) (Eq n))).

Definition up_subst_subst_tm_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_tm_ty tauty)) (up_tm_ty sigma)) x = (up_tm_ty theta) x :=
  fun n => (eq_trans) (compRenSubst_ty ((@id) (_)) (up_tm_ty tauty) ((funcomp) (up_tm_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_tm_tm { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (tauty : (fin) (lty) -> ty (mty)) (tautm : (fin) (ltm) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (subst_tm tauty tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_tm_ty tauty) (up_tm_tm tautm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
  fun n => match n with
  | Some fin_n => (eq_trans) (compRenSubst_tm ((@id) (_)) (shift) (up_tm_ty tauty) (up_tm_tm tautm) ((funcomp) (up_tm_ty tauty) ((@id) (_))) ((funcomp) (up_tm_tm tautm) (shift)) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tauty tautm ((@id) (_)) (shift) ((funcomp) (ren_ty ((@id) (_))) tauty) ((funcomp) (ren_tm ((@id) (_)) (shift)) tautm) (fun x => eq_refl) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)))
  | None => eq_refl
  end.

Definition up_subst_subst_list_ty_tm { p : nat } { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (tauty : (fin) (lty) -> ty (mty)) (tautm : (fin) (ltm) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (subst_tm tauty tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (upList_ty_ty p tauty) (upList_ty_tm p tautm)) (upList_ty_tm p sigma)) x = (upList_ty_tm p theta) x :=
  fun n => (eq_trans) (compRenSubst_tm (shift_p p) ((@id) (_)) (upList_ty_ty p tauty) (upList_ty_tm p tautm) ((funcomp) (upList_ty_ty p tauty) (shift_p p)) ((funcomp) (upList_ty_tm p tautm) ((@id) (_))) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tauty tautm (shift_p p) ((@id) (_)) (_) (_) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (fun x => (eq_sym) (eq_refl)) (sigma n))) ((ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n))).

Definition up_subst_subst_list_tm_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_tm_ty p tauty)) (upList_tm_ty p sigma)) x = (upList_tm_ty p theta) x :=
  fun n => (eq_trans) (compRenSubst_ty ((@id) (_)) (upList_tm_ty p tauty) ((funcomp) (upList_tm_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_tm_tm { p : nat } { k : nat } { lty ltm : nat } { mty mtm : nat } (sigma : (fin) (k) -> tm (lty) (ltm)) (tauty : (fin) (lty) -> ty (mty)) (tautm : (fin) (ltm) -> tm (mty) (mtm)) (theta : (fin) (k) -> tm (mty) (mtm)) (Eq : forall x, ((funcomp) (subst_tm tauty tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (upList_tm_ty p tauty) (upList_tm_tm p tautm)) (upList_tm_tm p sigma)) x = (upList_tm_tm p theta) x :=
  fun n => (eq_trans) (scons_p_comp' ((funcomp) (var_tm (lty) (p+ ltm)) (zero_p p)) (_) (_) n) (scons_p_congr (fun x => scons_p_head' (_) (fun z => ren_tm ((@id) (_)) (shift_p p) (_)) x) (fun n => (eq_trans) (compRenSubst_tm ((@id) (_)) (shift_p p) (upList_tm_ty p tauty) (upList_tm_tm p tautm) ((funcomp) (upList_tm_ty p tauty) ((@id) (_))) ((funcomp) (upList_tm_tm p tautm) (shift_p p)) (fun x => eq_refl) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tauty tautm ((@id) (_)) (shift_p p) (_) (_) (fun x => (eq_sym) (eq_refl)) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (sigma n))) ((ap) (ren_tm ((@id) (_)) (shift_p p)) (Eq n))))).

Fixpoint compSubstSubst_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) (thetaty : (fin) (mty) -> ty (lty)) (thetatm : (fin) (mtm) -> tm (lty) (ltm)) (Eqty : forall x, ((funcomp) (subst_ty tauty) sigmaty) x = thetaty x) (Eqtm : forall x, ((funcomp) (subst_tm tauty tautm) sigmatm) x = thetatm x) (s : tm (mty) (mtm)) : subst_tm tauty tautm (subst_tm sigmaty sigmatm s) = subst_tm thetaty thetatm s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((compSubstSubst_tm sigmaty sigmatm tauty tautm thetaty thetatm Eqty Eqtm) s0) ((compSubstSubst_tm sigmaty sigmatm tauty tautm thetaty thetatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((compSubstSubst_tm sigmaty sigmatm tauty tautm thetaty thetatm Eqty Eqtm) s0) ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((compSubstSubst_tm sigmaty sigmatm tauty tautm thetaty thetatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_tm (up_tm_ty sigmaty) (up_tm_tm sigmatm) (up_tm_ty tauty) (up_tm_tm tautm) (up_tm_ty thetaty) (up_tm_tm thetatm) (up_subst_subst_tm_ty (_) (_) (_) Eqty) (up_subst_subst_tm_tm (_) (_) (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((compSubstSubst_ty sigmaty tauty thetaty Eqty) s0) ((compSubstSubst_tm (up_ty_ty sigmaty) (up_ty_tm sigmatm) (up_ty_ty tauty) (up_ty_tm tautm) (up_ty_ty thetaty) (up_ty_tm thetatm) (up_subst_subst_ty_ty (_) (_) (_) Eqty) (up_subst_subst_ty_tm (_) (_) (_) (_) Eqtm)) s1)
    end.

Definition rinstInst_up_ty_tm { m : nat } { nty ntm : nat } (xi : (fin) (m) -> (fin) (ntm)) (sigma : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, ((funcomp) (var_tm (nty) (ntm)) xi) x = sigma x) : forall x, ((funcomp) (var_tm ((S) nty) (ntm)) (upRen_ty_tm xi)) x = (up_ty_tm sigma) x :=
  fun n => (ap) (ren_tm (shift) ((@id) (_))) (Eq n).

Definition rinstInst_up_tm_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_tm_ty xi)) x = (up_tm_ty sigma) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition rinstInst_up_tm_tm { m : nat } { nty ntm : nat } (xi : (fin) (m) -> (fin) (ntm)) (sigma : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, ((funcomp) (var_tm (nty) (ntm)) xi) x = sigma x) : forall x, ((funcomp) (var_tm (nty) ((S) ntm)) (upRen_tm_tm xi)) x = (up_tm_tm sigma) x :=
  fun n => match n with
  | Some fin_n => (ap) (ren_tm ((@id) (_)) (shift)) (Eq fin_n)
  | None => eq_refl
  end.

Definition rinstInst_up_list_ty_tm { p : nat } { m : nat } { nty ntm : nat } (xi : (fin) (m) -> (fin) (ntm)) (sigma : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, ((funcomp) (var_tm (nty) (ntm)) xi) x = sigma x) : forall x, ((funcomp) (var_tm (p+ nty) (ntm)) (upRenList_ty_tm p xi)) x = (upList_ty_tm p sigma) x :=
  fun n => (ap) (ren_tm (shift_p p) ((@id) (_))) (Eq n).

Definition rinstInst_up_list_tm_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_tm_ty p xi)) x = (upList_tm_ty p sigma) x :=
  fun n => (ap) (ren_ty ((@id) (_))) (Eq n).

Definition rinstInst_up_list_tm_tm { p : nat } { m : nat } { nty ntm : nat } (xi : (fin) (m) -> (fin) (ntm)) (sigma : (fin) (m) -> tm (nty) (ntm)) (Eq : forall x, ((funcomp) (var_tm (nty) (ntm)) xi) x = sigma x) : forall x, ((funcomp) (var_tm (nty) (p+ ntm)) (upRenList_tm_tm p xi)) x = (upList_tm_tm p sigma) x :=
  fun n => (eq_trans) (scons_p_comp' (_) (_) (var_tm (nty) (p+ ntm)) n) (scons_p_congr (fun z => eq_refl) (fun n => (ap) (ren_tm ((@id) (_)) (shift_p p)) (Eq n))).

Fixpoint rinst_inst_tm { mty mtm : nat } { nty ntm : nat } (xity : (fin) (mty) -> (fin) (nty)) (xitm : (fin) (mtm) -> (fin) (ntm)) (sigmaty : (fin) (mty) -> ty (nty)) (sigmatm : (fin) (mtm) -> tm (nty) (ntm)) (Eqty : forall x, ((funcomp) (var_ty (nty)) xity) x = sigmaty x) (Eqtm : forall x, ((funcomp) (var_tm (nty) (ntm)) xitm) x = sigmatm x) (s : tm (mty) (mtm)) : ren_tm xity xitm s = subst_tm sigmaty sigmatm s :=
    match s with
    | var_tm (_) (_) s => Eqtm s
    | app (_) (_) s0 s1 => congr_app ((rinst_inst_tm xity xitm sigmaty sigmatm Eqty Eqtm) s0) ((rinst_inst_tm xity xitm sigmaty sigmatm Eqty Eqtm) s1)
    | tapp (_) (_) s0 s1 => congr_tapp ((rinst_inst_tm xity xitm sigmaty sigmatm Eqty Eqtm) s0) ((rinst_inst_ty xity sigmaty Eqty) s1)
    | vt (_) (_) s0 => congr_vt ((rinst_inst_tm xity xitm sigmaty sigmatm Eqty Eqtm) s0)
    | abs (_) (_) s0 s1 => congr_abs ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_tm (upRen_tm_ty xity) (upRen_tm_tm xitm) (up_tm_ty sigmaty) (up_tm_tm sigmatm) (rinstInst_up_tm_ty (_) (_) Eqty) (rinstInst_up_tm_tm (_) (_) Eqtm)) s1)
    | tabs (_) (_) s0 s1 => congr_tabs ((rinst_inst_ty xity sigmaty Eqty) s0) ((rinst_inst_tm (upRen_ty_ty xity) (upRen_ty_tm xitm) (up_ty_ty sigmaty) (up_ty_tm sigmatm) (rinstInst_up_ty_ty (_) (_) Eqty) (rinstInst_up_ty_tm (_) (_) Eqtm)) s1)
    end.

Lemma rinstInst_tm { mty mtm : nat } { nty ntm : nat } (xity : (fin) (mty) -> (fin) (nty)) (xitm : (fin) (mtm) -> (fin) (ntm)) : ren_tm xity xitm = subst_tm ((funcomp) (var_ty (nty)) xity) ((funcomp) (var_tm (nty) (ntm)) xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_tm xity xitm (_) (_) (fun n => eq_refl) (fun n => eq_refl) x)). Qed.

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

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

Lemma varL_tm { mty mtm : nat } { nty ntm : nat } (sigmaty : (fin) (mty) -> ty (nty)) (sigmatm : (fin) (mtm) -> tm (nty) (ntm)) : (funcomp) (subst_tm sigmaty sigmatm) (var_tm (mty) (mtm)) = sigmatm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma varLRen_tm { mty mtm : nat } { nty ntm : nat } (xity : (fin) (mty) -> (fin) (nty)) (xitm : (fin) (mtm) -> (fin) (ntm)) : (funcomp) (ren_tm xity xitm) (var_tm (mty) (mtm)) = (funcomp) (var_tm (nty) (ntm)) xitm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.

Lemma compComp_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) (s : tm (mty) (mtm)) : subst_tm tauty tautm (subst_tm sigmaty sigmatm s) = subst_tm ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_tm tauty tautm) sigmatm) s .
Proof. exact (compSubstSubst_tm sigmaty sigmatm tauty tautm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compComp'_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) : (funcomp) (subst_tm tauty tautm) (subst_tm sigmaty sigmatm) = subst_tm ((funcomp) (subst_ty tauty) sigmaty) ((funcomp) (subst_tm tauty tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmaty sigmatm tauty tautm n)). Qed.

Lemma compRen_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (s : tm (mty) (mtm)) : ren_tm zetaty zetatm (subst_tm sigmaty sigmatm s) = subst_tm ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_tm zetaty zetatm) sigmatm) s .
Proof. exact (compSubstRen_tm sigmaty sigmatm zetaty zetatm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma compRen'_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (sigmaty : (fin) (mty) -> ty (kty)) (sigmatm : (fin) (mtm) -> tm (kty) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) : (funcomp) (ren_tm zetaty zetatm) (subst_tm sigmaty sigmatm) = subst_tm ((funcomp) (ren_ty zetaty) sigmaty) ((funcomp) (ren_tm zetaty zetatm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_tm sigmaty sigmatm zetaty zetatm n)). Qed.

Lemma renComp_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) (s : tm (mty) (mtm)) : subst_tm tauty tautm (ren_tm xity xitm s) = subst_tm ((funcomp) tauty xity) ((funcomp) tautm xitm) s .
Proof. exact (compRenSubst_tm xity xitm tauty tautm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renComp'_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (tauty : (fin) (kty) -> ty (lty)) (tautm : (fin) (ktm) -> tm (lty) (ltm)) : (funcomp) (subst_tm tauty tautm) (ren_tm xity xitm) = subst_tm ((funcomp) tauty xity) ((funcomp) tautm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_tm xity xitm tauty tautm n)). Qed.

Lemma renRen_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (s : tm (mty) (mtm)) : ren_tm zetaty zetatm (ren_tm xity xitm s) = ren_tm ((funcomp) zetaty xity) ((funcomp) zetatm xitm) s .
Proof. exact (compRenRen_tm xity xitm zetaty zetatm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.

Lemma renRen'_tm { kty ktm : nat } { lty ltm : nat } { mty mtm : nat } (xity : (fin) (mty) -> (fin) (kty)) (xitm : (fin) (mtm) -> (fin) (ktm)) (zetaty : (fin) (kty) -> (fin) (lty)) (zetatm : (fin) (ktm) -> (fin) (ltm)) : (funcomp) (ren_tm zetaty zetatm) (ren_tm xity xitm) = ren_tm ((funcomp) zetaty xity) ((funcomp) zetatm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_tm xity xitm zetaty zetatm n)). Qed.

Arguments var_ty {nty}.

Arguments top {nty}.

Arguments arr {nty}.

Arguments all {nty}.

Arguments var_tm {nty} {ntm}.

Arguments app {nty} {ntm}.

Arguments tapp {nty} {ntm}.

Arguments vt {nty} {ntm}.

Arguments abs {nty} {ntm}.

Arguments tabs {nty} {ntm}.

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

Instance Subst_tm { mty mtm : nat } { nty ntm : nat } : Subst2 ((fin) (mty) -> ty (nty)) ((fin) (mtm) -> tm (nty) (ntm)) (tm (mty) (mtm)) (tm (nty) (ntm)) := @subst_tm (mty) (mtm) (nty) (ntm) .

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

Instance Ren_tm { mty mtm : nat } { nty ntm : nat } : Ren2 ((fin) (mty) -> (fin) (nty)) ((fin) (mtm) -> (fin) (ntm)) (tm (mty) (mtm)) (tm (nty) (ntm)) := @ren_tm (mty) (mtm) (nty) (ntm) .

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.

Instance VarInstance_tm { mty mtm : nat } : Var ((fin) (mtm)) (tm (mty) (mtm)) := @var_tm (mty) (mtm) .

Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.

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

Notation "'var'" := (var_tm) (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_tm X Y := up_tm : X -> Y.

Notation "↑__tm" := (up_tm) (only printing) : subst_scope.

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

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

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

Instance Up_ty_tm { m : nat } { nty ntm : nat } : Up_tm (_) (_) := @up_ty_tm (m) (nty) (ntm) .

Notation "↑__tm" := (up_tm_ty) (only printing) : subst_scope.

Instance Up_tm_ty { m : nat } { nty : nat } : Up_ty (_) (_) := @up_tm_ty (m) (nty) .

Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.

Instance Up_tm_tm { m : nat } { nty ntm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (nty) (ntm) .

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

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

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

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

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

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

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

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

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

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

Ltac asimpl' := repeat first [progress rewrite ?instId_ty| progress rewrite ?rinstId_ty| progress rewrite ?compComp_ty| progress rewrite ?compComp'_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 ?instId_tm| progress rewrite ?rinstId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_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 ?varL_ty| progress rewrite ?varLRen_ty| progress rewrite ?varL_tm| progress rewrite ?varLRen_tm| progress (unfold up_ren, upRen_ty_ty, upRenList_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, upRenList_ty_tm, upRenList_tm_ty, upRenList_tm_tm, up_ty_ty, upList_ty_ty, up_ty_tm, up_tm_ty, up_tm_tm, upList_ty_tm, upList_tm_ty, upList_tm_tm)| progress (cbn [subst_ty subst_tm ren_ty ren_tm])| 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 ?rinstId_ty in *| progress rewrite ?compComp_ty in *| progress rewrite ?compComp'_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 ?instId_tm in *| progress rewrite ?rinstId_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_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 ?varL_ty in *| progress rewrite ?varLRen_ty in *| progress rewrite ?varL_tm in *| progress rewrite ?varLRen_tm in *| progress (unfold up_ren, upRen_ty_ty, upRenList_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, upRenList_ty_tm, upRenList_tm_ty, upRenList_tm_tm, up_ty_ty, upList_ty_ty, up_ty_tm, up_tm_ty, up_tm_tm, upList_ty_tm, upList_tm_ty, upList_tm_tm in *)| progress (cbn [subst_ty subst_tm ren_ty ren_tm] in *)| fsimpl in *].

Ltac substify := auto_unfold; try repeat (erewrite rinst_inst_ty; [|now intros]); try repeat (erewrite rinst_inst_tm; [|now intros]).

Ltac renamify := auto_unfold; try repeat (erewrite <- rinst_inst_ty; [|intros; now asimpl]); try repeat (erewrite <- rinst_inst_tm; [|intros; now asimpl]).