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).
Lemma congr_top { mty : nat } : top (mty) = top (mty) .
Proof. congruence. Qed.
Lemma congr_arr { mty : nat } { s0 : ty (mty) } { s1 : ty (mty) } { t0 : ty (mty) } { t1 : ty (mty) } : s0 = t0 -> s1 = t1 -> arr (mty) s0 s1 = arr (mty) t0 t1 .
Proof. congruence. Qed.
Lemma congr_all { mty : nat } { s0 : ty (mty) } { s1 : ty (S mty) } { t0 : ty (mty) } { t1 : ty (S mty) } : s0 = t0 -> s1 = t1 -> all (mty) s0 s1 = all (mty) t0 t1 .
Proof. congruence. Qed.
Definition upRen_ty_ty { m : nat } { n : nat } (xi : fin (m) -> fin (n)) : _ :=
up_ren 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).
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => ap shift (Eq n)
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => eq_trans (compRenRen_ty shift (upRen_ty_ty zetaty) (funcomp shift zetaty) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_ty zetaty shift (funcomp shift zetaty) (fun x => eq_refl) (sigma n))) (ap (ren_ty shift) (Eq n)))
| None => eq_refl
end.
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 n => eq_trans (compRenSubst_ty shift (up_ty_ty tauty) (funcomp (up_ty_ty tauty) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__ty tauty shift (funcomp (ren_ty shift) tauty) (fun x => eq_refl) (sigma n))) (ap (ren_ty shift) (Eq n)))
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 .
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.
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).
Lemma congr_app { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } { t1 : tm (mty) (mtm) } : s0 = t0 -> s1 = t1 -> app (mty) (mtm) s0 s1 = app (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tapp { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : ty (mty) } { t0 : tm (mty) (mtm) } { t1 : ty (mty) } : s0 = t0 -> s1 = t1 -> tapp (mty) (mtm) s0 s1 = tapp (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_vt { mty mtm : nat } { s0 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } : s0 = t0 -> vt (mty) (mtm) s0 = vt (mty) (mtm) t0 .
Proof. congruence. Qed.
Lemma congr_abs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm (mty) (S mtm) } { t0 : ty (mty) } { t1 : tm (mty) (S mtm) } : s0 = t0 -> s1 = t1 -> abs (mty) (mtm) s0 s1 = abs (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tabs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm (S mty) (mtm) } { t0 : ty (mty) } { t1 : tm (S mty) (mtm) } : s0 = t0 -> s1 = t1 -> tabs (mty) (mtm) s0 s1 = tabs (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
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.
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).
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 n => ap shift (Eq n)
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 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 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 n))) (ap (ren_tm id shift) (Eq n)))
| None => eq_refl
end.
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 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 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 n))) (ap (ren_tm id shift) (Eq n)))
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 .
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 x))). Qed.
Lemma rinstId_tm { mty mtm : nat } : @ren_tm (mty) (mtm) (mty) (mtm) id id = id .
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.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_tm) (only printing) : subst_scope.
Notation "⇑__tm" := (up_tm_ty) (only printing) : subst_scope.
Notation "⇑__tm" := (up_tm_tm) (only printing) : subst_scope.
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, upRen_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, up_ty_ty, up_ty_ty, up_ty_tm, up_tm_ty, up_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, upRen_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, up_ty_ty, up_ty_ty, up_ty_tm, up_tm_ty, up_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]).
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).
Lemma congr_top { mty : nat } : top (mty) = top (mty) .
Proof. congruence. Qed.
Lemma congr_arr { mty : nat } { s0 : ty (mty) } { s1 : ty (mty) } { t0 : ty (mty) } { t1 : ty (mty) } : s0 = t0 -> s1 = t1 -> arr (mty) s0 s1 = arr (mty) t0 t1 .
Proof. congruence. Qed.
Lemma congr_all { mty : nat } { s0 : ty (mty) } { s1 : ty (S mty) } { t0 : ty (mty) } { t1 : ty (S mty) } : s0 = t0 -> s1 = t1 -> all (mty) s0 s1 = all (mty) t0 t1 .
Proof. congruence. Qed.
Definition upRen_ty_ty { m : nat } { n : nat } (xi : fin (m) -> fin (n)) : _ :=
up_ren 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).
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => ap shift (Eq n)
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 n => eq_trans (compRenRen_ty shift (upRen_ty_ty zetaty) (funcomp shift zetaty) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_ty zetaty shift (funcomp shift zetaty) (fun x => eq_refl) (sigma n))) (ap (ren_ty shift) (Eq n)))
| None => eq_refl
end.
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 n => eq_trans (compRenSubst_ty shift (up_ty_ty tauty) (funcomp (up_ty_ty tauty) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__ty tauty shift (funcomp (ren_ty shift) tauty) (fun x => eq_refl) (sigma n))) (ap (ren_ty shift) (Eq n)))
| None => eq_refl
end.
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 n => ap (ren_ty shift) (Eq n)
| None => eq_refl
end.
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 .
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.
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).
Lemma congr_app { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } { t1 : tm (mty) (mtm) } : s0 = t0 -> s1 = t1 -> app (mty) (mtm) s0 s1 = app (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tapp { mty mtm : nat } { s0 : tm (mty) (mtm) } { s1 : ty (mty) } { t0 : tm (mty) (mtm) } { t1 : ty (mty) } : s0 = t0 -> s1 = t1 -> tapp (mty) (mtm) s0 s1 = tapp (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_vt { mty mtm : nat } { s0 : tm (mty) (mtm) } { t0 : tm (mty) (mtm) } : s0 = t0 -> vt (mty) (mtm) s0 = vt (mty) (mtm) t0 .
Proof. congruence. Qed.
Lemma congr_abs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm (mty) (S mtm) } { t0 : ty (mty) } { t1 : tm (mty) (S mtm) } : s0 = t0 -> s1 = t1 -> abs (mty) (mtm) s0 s1 = abs (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tabs { mty mtm : nat } { s0 : ty (mty) } { s1 : tm (S mty) (mtm) } { t0 : ty (mty) } { t1 : tm (S mty) (mtm) } : s0 = t0 -> s1 = t1 -> tabs (mty) (mtm) s0 s1 = tabs (mty) (mtm) t0 t1 .
Proof. congruence. Qed.
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.
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).
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 n => ap shift (Eq n)
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 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 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 n))) (ap (ren_tm id shift) (Eq n)))
| None => eq_refl
end.
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 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 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 n))) (ap (ren_tm id shift) (Eq n)))
| None => eq_refl
end.
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 n => ap (ren_tm id shift) (Eq n)
| None => eq_refl
end.
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 .
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 x))). Qed.
Lemma rinstId_tm { mty mtm : nat } : @ren_tm (mty) (mtm) (mty) (mtm) id id = id .
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.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_tm) (only printing) : subst_scope.
Notation "⇑__tm" := (up_tm_ty) (only printing) : subst_scope.
Notation "⇑__tm" := (up_tm_tm) (only printing) : subst_scope.
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, upRen_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, up_ty_ty, up_ty_ty, up_ty_tm, up_tm_ty, up_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, upRen_ty_ty, upRen_ty_tm, upRen_tm_ty, upRen_tm_tm, up_ty_ty, up_ty_ty, up_ty_tm, up_tm_ty, up_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]).