Library Autosubst.SystemFCBV
Require Export fintype.
Inductive ty (nty : nat) : Type :=
| var_ty : fin (nty) → ty (nty)
| arr : ty (nty) → ty (nty) → ty (nty)
| all : ty (S nty) → ty (nty).
Lemma congr_arr { mty : nat } { s0 : ty (mty) } { s1 : ty (mty) } { t0 : ty (mty) } { t1 : ty (mty) } : s0 = t0 → s1 = t1 → arr (mty) s0 s1 = arr (mty) t0 t1 .
Proof. congruence. Qed.
Lemma congr_all { mty : nat } { s0 : ty (S mty) } { t0 : ty (S mty) } : s0 = t0 → all (mty) s0 = all (mty) t0 .
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)
| arr (_) s0 s1 ⇒ arr (nty) (ren_ty xity s0) (ren_ty xity s1)
| all (_) s0 ⇒ all (nty) (ren_ty (upRen_ty_ty xity) s0)
end.
Definition up_ty_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) : _ :=
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
| arr (_) s0 s1 ⇒ arr (nty) (subst_ty sigmaty s0) (subst_ty sigmaty s1)
| all (_) s0 ⇒ all (nty) (subst_ty (up_ty_ty sigmaty) s0)
end.
Definition upId_ty_ty { mty : nat } (sigma : fin (mty) → ty (mty)) (Eq : ∀ x, sigma x = (var_ty (mty)) x) : ∀ 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 : ∀ x, sigmaty x = (var_ty (mty)) x) (s : ty (mty)) : subst_ty sigmaty s = s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (idSubst_ty sigmaty Eqty s0) (idSubst_ty sigmaty Eqty s1)
| all (_) s0 ⇒ congr_all (idSubst_ty (up_ty_ty sigmaty) (upId_ty_ty (_) Eqty) s0)
end.
Definition upExtRen_ty_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ 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 : ∀ x, xity x = zetaty x) (s : ty (mty)) : ren_ty xity s = ren_ty zetaty s :=
match s with
| var_ty (_) s ⇒ ap (var_ty (nty)) (Eqty s)
| arr (_) s0 s1 ⇒ congr_arr (extRen_ty xity zetaty Eqty s0) (extRen_ty xity zetaty Eqty s1)
| all (_) s0 ⇒ congr_all (extRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upExtRen_ty_ty (_) (_) Eqty) s0)
end.
Definition upExt_ty_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) (tau : fin (m) → ty (nty)) (Eq : ∀ x, sigma x = tau x) : ∀ 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 : ∀ x, sigmaty x = tauty x) (s : ty (mty)) : subst_ty sigmaty s = subst_ty tauty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (ext_ty sigmaty tauty Eqty s0) (ext_ty sigmaty tauty Eqty s1)
| all (_) s0 ⇒ congr_all (ext_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (upExt_ty_ty (_) (_) Eqty) s0)
end.
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 : ∀ x, (funcomp zetaty xity) x = rhoty x) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty rhoty s :=
match s with
| var_ty (_) s ⇒ ap (var_ty (lty)) (Eqty s)
| arr (_) s0 s1 ⇒ congr_arr (compRenRen_ty xity zetaty rhoty Eqty s0) (compRenRen_ty xity zetaty rhoty Eqty s1)
| all (_) s0 ⇒ congr_all (compRenRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upRen_ty_ty rhoty) (up_ren_ren (_) (_) (_) Eqty) s0)
end.
Definition up_ren_subst_ty_ty { k : nat } { l : nat } { mty : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ 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 : ∀ x, (funcomp tauty xity) x = thetaty x) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compRenSubst_ty xity tauty thetaty Eqty s0) (compRenSubst_ty xity tauty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compRenSubst_ty (upRen_ty_ty xity) (up_ty_ty tauty) (up_ty_ty thetaty) (up_ren_subst_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition up_subst_ren_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (zetaty : fin (lty) → fin (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (ren_ty zetaty) sigma) x = theta x) : ∀ 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 : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compSubstRen__ty sigmaty zetaty thetaty Eqty s0) (compSubstRen__ty sigmaty zetaty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compSubstRen__ty (up_ty_ty sigmaty) (upRen_ty_ty zetaty) (up_ty_ty thetaty) (up_subst_ren_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition up_subst_subst_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (tauty : fin (lty) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (subst_ty tauty) sigma) x = theta x) : ∀ 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 : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compSubstSubst_ty sigmaty tauty thetaty Eqty s0) (compSubstSubst_ty sigmaty tauty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compSubstSubst_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (up_ty_ty thetaty) (up_subst_subst_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition rinstInst_up_ty_ty { m : nat } { nty : nat } (xi : fin (m) → fin (nty)) (sigma : fin (m) → ty (nty)) (Eq : ∀ x, (funcomp (var_ty (nty)) xi) x = sigma x) : ∀ 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 : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (s : ty (mty)) : ren_ty xity s = subst_ty sigmaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (rinst_inst_ty xity sigmaty Eqty s0) (rinst_inst_ty xity sigmaty Eqty s1)
| all (_) s0 ⇒ congr_all (rinst_inst_ty (upRen_ty_ty xity) (up_ty_ty sigmaty) (rinstInst_up_ty_ty (_) (_) Eqty) s0)
end.
Lemma rinstInst_ty { mty : nat } { nty : nat } (xity : fin (mty) → fin (nty)) : ren_ty xity = subst_ty (funcomp (var_ty (nty)) xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_ty xity (_) (fun n ⇒ eq_refl) x)). Qed.
Lemma instId_ty { mty : nat } : subst_ty (var_ty (mty)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_ty (var_ty (mty)) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma rinstId_ty { mty : nat } : @ren_ty (mty) (mty) id = id .
Proof. exact (eq_trans (rinstInst_ty id) instId_ty). Qed.
Lemma varL_ty { mty : nat } { nty : nat } (sigmaty : fin (mty) → ty (nty)) : funcomp (subst_ty sigmaty) (var_ty (mty)) = sigmaty .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma varLRen_ty { mty : nat } { nty : nat } (xity : fin (mty) → fin (nty)) : funcomp (ren_ty xity) (var_ty (mty)) = funcomp (var_ty (nty)) xity .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma compComp_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (tauty : fin (kty) → ty (lty)) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty (funcomp (subst_ty tauty) sigmaty) s .
Proof. exact (compSubstSubst_ty sigmaty tauty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (tauty : fin (kty) → ty (lty)) : funcomp (subst_ty tauty) (subst_ty sigmaty) = subst_ty (funcomp (subst_ty tauty) sigmaty) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_ty sigmaty tauty n)). Qed.
Lemma compRen_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (zetaty : fin (kty) → fin (lty)) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty (funcomp (ren_ty zetaty) sigmaty) s .
Proof. exact (compSubstRen__ty sigmaty zetaty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (zetaty : fin (kty) → fin (lty)) : funcomp (ren_ty zetaty) (subst_ty sigmaty) = subst_ty (funcomp (ren_ty zetaty) sigmaty) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_ty sigmaty zetaty n)). Qed.
Lemma renComp_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (tauty : fin (kty) → ty (lty)) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty (funcomp tauty xity) s .
Proof. exact (compRenSubst_ty xity tauty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp'_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (tauty : fin (kty) → ty (lty)) : funcomp (subst_ty tauty) (ren_ty xity) = subst_ty (funcomp tauty xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_ty xity tauty n)). Qed.
Lemma renRen_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (zetaty : fin (kty) → fin (lty)) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty (funcomp zetaty xity) s .
Proof. exact (compRenRen_ty xity zetaty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen'_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (zetaty : fin (kty) → fin (lty)) : funcomp (ren_ty zetaty) (ren_ty xity) = ren_ty (funcomp zetaty xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_ty xity zetaty n)). Qed.
Inductive tm (nty nvl : nat) : Type :=
| app : tm (nty) (nvl) → tm (nty) (nvl) → tm (nty) (nvl)
| tapp : tm (nty) (nvl) → ty (nty) → tm (nty) (nvl)
| vt : vl (nty) (nvl) → tm (nty) (nvl)
with vl (nty nvl : nat) : Type :=
| var_vl : fin (nvl) → vl (nty) (nvl)
| lam : ty (nty) → tm (nty) (S nvl) → vl (nty) (nvl)
| tlam : tm (S nty) (nvl) → vl (nty) (nvl).
Lemma congr_app { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : tm (mty) (mvl) } { t0 : tm (mty) (mvl) } { t1 : tm (mty) (mvl) } : s0 = t0 → s1 = t1 → app (mty) (mvl) s0 s1 = app (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tapp { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : ty (mty) } { t0 : tm (mty) (mvl) } { t1 : ty (mty) } : s0 = t0 → s1 = t1 → tapp (mty) (mvl) s0 s1 = tapp (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_vt { mty mvl : nat } { s0 : vl (mty) (mvl) } { t0 : vl (mty) (mvl) } : s0 = t0 → vt (mty) (mvl) s0 = vt (mty) (mvl) t0 .
Proof. congruence. Qed.
Lemma congr_lam { mty mvl : nat } { s0 : ty (mty) } { s1 : tm (mty) (S mvl) } { t0 : ty (mty) } { t1 : tm (mty) (S mvl) } : s0 = t0 → s1 = t1 → lam (mty) (mvl) s0 s1 = lam (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tlam { mty mvl : nat } { s0 : tm (S mty) (mvl) } { t0 : tm (S mty) (mvl) } : s0 = t0 → tlam (mty) (mvl) s0 = tlam (mty) (mvl) t0 .
Proof. congruence. Qed.
Definition upRen_ty_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
xi.
Definition upRen_vl_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
xi.
Definition upRen_vl_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
up_ren xi.
Fixpoint ren_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (s : tm (mty) (mvl)) : _ :=
match s with
| app (_) (_) s0 s1 ⇒ app (nty) (nvl) (ren_tm xity xivl s0) (ren_tm xity xivl s1)
| tapp (_) (_) s0 s1 ⇒ tapp (nty) (nvl) (ren_tm xity xivl s0) (ren_ty xity s1)
| vt (_) (_) s0 ⇒ vt (nty) (nvl) (ren_vl xity xivl s0)
end
with ren_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (s : vl (mty) (mvl)) : _ :=
match s with
| var_vl (_) (_) s ⇒ (var_vl (nty) (nvl)) (xivl s)
| lam (_) (_) s0 s1 ⇒ lam (nty) (nvl) (ren_ty xity s0) (ren_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) s1)
| tlam (_) (_) s0 ⇒ tlam (nty) (nvl) (ren_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) s0)
end.
Definition up_ty_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) : _ :=
funcomp (ren_vl shift id) sigma.
Definition up_vl_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) : _ :=
funcomp (ren_ty id) sigma.
Definition up_vl_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) : _ :=
scons ((var_vl (nty) (S nvl)) var_zero) (funcomp (ren_vl id shift) sigma).
Fixpoint subst_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (s : tm (mty) (mvl)) : _ :=
match s with
| app (_) (_) s0 s1 ⇒ app (nty) (nvl) (subst_tm sigmaty sigmavl s0) (subst_tm sigmaty sigmavl s1)
| tapp (_) (_) s0 s1 ⇒ tapp (nty) (nvl) (subst_tm sigmaty sigmavl s0) (subst_ty sigmaty s1)
| vt (_) (_) s0 ⇒ vt (nty) (nvl) (subst_vl sigmaty sigmavl s0)
end
with subst_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (s : vl (mty) (mvl)) : _ :=
match s with
| var_vl (_) (_) s ⇒ sigmavl s
| lam (_) (_) s0 s1 ⇒ lam (nty) (nvl) (subst_ty sigmaty s0) (subst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) s1)
| tlam (_) (_) s0 ⇒ tlam (nty) (nvl) (subst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) s0)
end.
Definition upId_ty_vl { mty mvl : nat } (sigma : fin (mvl) → vl (mty) (mvl)) (Eq : ∀ x, sigma x = (var_vl (mty) (mvl)) x) : ∀ x, (up_ty_vl sigma) x = (var_vl (S mty) (mvl)) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition upId_vl_ty { mty : nat } (sigma : fin (mty) → ty (mty)) (Eq : ∀ x, sigma x = (var_ty (mty)) x) : ∀ x, (up_vl_ty sigma) x = (var_ty (mty)) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition upId_vl_vl { mty mvl : nat } (sigma : fin (mvl) → vl (mty) (mvl)) (Eq : ∀ x, sigma x = (var_vl (mty) (mvl)) x) : ∀ x, (up_vl_vl sigma) x = (var_vl (mty) (S mvl)) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint idSubst_tm { mty mvl : nat } (sigmaty : fin (mty) → ty (mty)) (sigmavl : fin (mvl) → vl (mty) (mvl)) (Eqty : ∀ x, sigmaty x = (var_ty (mty)) x) (Eqvl : ∀ x, sigmavl x = (var_vl (mty) (mvl)) x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (idSubst_tm sigmaty sigmavl Eqty Eqvl s0) (idSubst_tm sigmaty sigmavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (idSubst_tm sigmaty sigmavl Eqty Eqvl s0) (idSubst_ty sigmaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (idSubst_vl sigmaty sigmavl Eqty Eqvl s0)
end
with idSubst_vl { mty mvl : nat } (sigmaty : fin (mty) → ty (mty)) (sigmavl : fin (mvl) → vl (mty) (mvl)) (Eqty : ∀ x, sigmaty x = (var_ty (mty)) x) (Eqvl : ∀ x, sigmavl x = (var_vl (mty) (mvl)) x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (idSubst_ty sigmaty Eqty s0) (idSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upId_vl_ty (_) Eqty) (upId_vl_vl (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (idSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upId_ty_ty (_) Eqty) (upId_ty_vl (_) Eqvl) s0)
end.
Definition upExtRen_ty_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_ty_vl xi) x = (upRen_ty_vl zeta) x :=
fun n ⇒ Eq n.
Definition upExtRen_vl_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_vl_ty xi) x = (upRen_vl_ty zeta) x :=
fun n ⇒ Eq n.
Definition upExtRen_vl_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_vl_vl xi) x = (upRen_vl_vl zeta) x :=
fun n ⇒ match n with
| Some n ⇒ ap shift (Eq n)
| None ⇒ eq_refl
end.
Fixpoint extRen_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (zetaty : fin (mty) → fin (nty)) (zetavl : fin (mvl) → fin (nvl)) (Eqty : ∀ x, xity x = zetaty x) (Eqvl : ∀ x, xivl x = zetavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = ren_tm zetaty zetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s0) (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s0) (extRen_ty xity zetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (extRen_vl xity xivl zetaty zetavl Eqty Eqvl s0)
end
with extRen_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (zetaty : fin (mty) → fin (nty)) (zetavl : fin (mvl) → fin (nvl)) (Eqty : ∀ x, xity x = zetaty x) (Eqvl : ∀ x, xivl x = zetavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = ren_vl zetaty zetavl s :=
match s with
| var_vl (_) (_) s ⇒ ap (var_vl (nty) (nvl)) (Eqvl s)
| lam (_) (_) s0 s1 ⇒ congr_lam (extRen_ty xity zetaty Eqty s0) (extRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upExtRen_vl_ty (_) (_) Eqty) (upExtRen_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (extRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upExtRen_ty_ty (_) (_) Eqty) (upExtRen_ty_vl (_) (_) Eqvl) s0)
end.
Definition upExt_ty_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) (tau : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_ty_vl sigma) x = (up_ty_vl tau) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition upExt_vl_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) (tau : fin (m) → ty (nty)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_vl_ty sigma) x = (up_vl_ty tau) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition upExt_vl_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) (tau : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_vl_vl sigma) x = (up_vl_vl tau) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint ext_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (tauty : fin (mty) → ty (nty)) (tauvl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, sigmaty x = tauty x) (Eqvl : ∀ x, sigmavl x = tauvl x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = subst_tm tauty tauvl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s0) (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s0) (ext_ty sigmaty tauty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (ext_vl sigmaty sigmavl tauty tauvl Eqty Eqvl s0)
end
with ext_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (tauty : fin (mty) → ty (nty)) (tauvl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, sigmaty x = tauty x) (Eqvl : ∀ x, sigmavl x = tauvl x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = subst_vl tauty tauvl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (ext_ty sigmaty tauty Eqty s0) (ext_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (upExt_vl_ty (_) (_) Eqty) (upExt_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (ext_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (upExt_ty_ty (_) (_) Eqty) (upExt_ty_vl (_) (_) Eqvl) s0)
end.
Fixpoint compRenRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (rhoty : fin (mty) → fin (lty)) (rhovl : fin (mvl) → fin (lvl)) (Eqty : ∀ x, (funcomp zetaty xity) x = rhoty x) (Eqvl : ∀ x, (funcomp zetavl xivl) x = rhovl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm rhoty rhovl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0) (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0) (compRenRen_ty xity zetaty rhoty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compRenRen_vl xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0)
end
with compRenRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (rhoty : fin (mty) → fin (lty)) (rhovl : fin (mvl) → fin (lvl)) (Eqty : ∀ x, (funcomp zetaty xity) x = rhoty x) (Eqvl : ∀ x, (funcomp zetavl xivl) x = rhovl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl rhoty rhovl s :=
match s with
| var_vl (_) (_) s ⇒ ap (var_vl (lty) (lvl)) (Eqvl s)
| lam (_) (_) s0 s1 ⇒ congr_lam (compRenRen_ty xity zetaty rhoty Eqty s0) (compRenRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upRen_vl_ty rhoty) (upRen_vl_vl rhovl) Eqty (up_ren_ren (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compRenRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upRen_ty_ty rhoty) (upRen_ty_vl rhovl) (up_ren_ren (_) (_) (_) Eqty) Eqvl s0)
end.
Definition up_ren_subst_ty_vl { k : nat } { l : nat } { mty mvl : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_ty_vl tau) (upRen_ty_vl xi)) x = (up_ty_vl theta) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition up_ren_subst_vl_ty { k : nat } { l : nat } { mty : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_vl_ty tau) (upRen_vl_ty xi)) x = (up_vl_ty theta) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition up_ren_subst_vl_vl { k : nat } { l : nat } { mty mvl : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_vl_vl tau) (upRen_vl_vl xi)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint compRenSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp tauty xity) x = thetaty x) (Eqvl : ∀ x, (funcomp tauvl xivl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compRenSubst_ty xity tauty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compRenSubst_vl xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0)
end
with compRenSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp tauty xity) x = thetaty x) (Eqvl : ∀ x, (funcomp tauvl xivl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compRenSubst_ty xity tauty thetaty Eqty s0) (compRenSubst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_ren_subst_vl_ty (_) (_) (_) Eqty) (up_ren_subst_vl_vl (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compRenSubst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_ren_subst_ty_ty (_) (_) (_) Eqty) (up_ren_subst_ty_vl (_) (_) (_) Eqvl) s0)
end.
Definition up_subst_ren_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (zetaty : fin (lty) → fin (mty)) (zetavl : fin (lvl) → fin (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (ren_vl zetaty zetavl) sigma) x = theta x) : ∀ x, (funcomp (ren_vl (upRen_ty_ty zetaty) (upRen_ty_vl zetavl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
fun n ⇒ eq_trans (compRenRen_vl shift id (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (funcomp shift zetaty) (funcomp id zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_vl zetaty zetavl shift id (funcomp shift zetaty) (funcomp id zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl shift id) (Eq n))).
Definition up_subst_ren_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (zetaty : fin (lty) → fin (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (ren_ty zetaty) sigma) x = theta x) : ∀ x, (funcomp (ren_ty (upRen_vl_ty zetaty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
fun n ⇒ eq_trans (compRenRen_ty id (upRen_vl_ty zetaty) (funcomp id zetaty) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_ty zetaty id (funcomp id zetaty) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_ty id) (Eq n))).
Definition up_subst_ren_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (zetaty : fin (lty) → fin (mty)) (zetavl : fin (lvl) → fin (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (ren_vl zetaty zetavl) sigma) x = theta x) : ∀ x, (funcomp (ren_vl (upRen_vl_ty zetaty) (upRen_vl_vl zetavl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ eq_trans (compRenRen_vl id shift (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (funcomp id zetaty) (funcomp shift zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_vl zetaty zetavl id shift (funcomp id zetaty) (funcomp shift zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl id shift) (Eq n)))
| None ⇒ eq_refl
end.
Fixpoint compSubstRen__tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0) (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0) (compSubstRen__ty sigmaty zetaty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compSubstRen__vl sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0)
end
with compSubstRen__vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compSubstRen__ty sigmaty zetaty thetaty Eqty s0) (compSubstRen__tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_ren_vl_ty (_) (_) (_) Eqty) (up_subst_ren_vl_vl (_) (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compSubstRen__tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_ren_ty_ty (_) (_) (_) Eqty) (up_subst_ren_ty_vl (_) (_) (_) (_) Eqvl) s0)
end.
Definition up_subst_subst_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (tauty : fin (lty) → ty (mty)) (tauvl : fin (lvl) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (subst_vl tauty tauvl) sigma) x = theta x) : ∀ x, (funcomp (subst_vl (up_ty_ty tauty) (up_ty_vl tauvl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
fun n ⇒ eq_trans (compRenSubst_vl shift id (up_ty_ty tauty) (up_ty_vl tauvl) (funcomp (up_ty_ty tauty) shift) (funcomp (up_ty_vl tauvl) id) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__vl tauty tauvl shift id (funcomp (ren_ty shift) tauty) (funcomp (ren_vl shift id) tauvl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl shift id) (Eq n))).
Definition up_subst_subst_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (tauty : fin (lty) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (subst_ty tauty) sigma) x = theta x) : ∀ x, (funcomp (subst_ty (up_vl_ty tauty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
fun n ⇒ eq_trans (compRenSubst_ty id (up_vl_ty tauty) (funcomp (up_vl_ty tauty) id) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__ty tauty id (funcomp (ren_ty id) tauty) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_ty id) (Eq n))).
Definition up_subst_subst_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (tauty : fin (lty) → ty (mty)) (tauvl : fin (lvl) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (subst_vl tauty tauvl) sigma) x = theta x) : ∀ x, (funcomp (subst_vl (up_vl_ty tauty) (up_vl_vl tauvl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ eq_trans (compRenSubst_vl id shift (up_vl_ty tauty) (up_vl_vl tauvl) (funcomp (up_vl_ty tauty) id) (funcomp (up_vl_vl tauvl) shift) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__vl tauty tauvl id shift (funcomp (ren_ty id) tauty) (funcomp (ren_vl id shift) tauvl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl id shift) (Eq n)))
| None ⇒ eq_refl
end.
Fixpoint compSubstSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compSubstSubst_ty sigmaty tauty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compSubstSubst_vl sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0)
end
with compSubstSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compSubstSubst_ty sigmaty tauty thetaty Eqty s0) (compSubstSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_subst_vl_ty (_) (_) (_) Eqty) (up_subst_subst_vl_vl (_) (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compSubstSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_subst_ty_ty (_) (_) (_) Eqty) (up_subst_subst_ty_vl (_) (_) (_) (_) Eqvl) s0)
end.
Definition rinstInst_up_ty_vl { m : nat } { nty nvl : nat } (xi : fin (m) → fin (nvl)) (sigma : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, (funcomp (var_vl (nty) (nvl)) xi) x = sigma x) : ∀ x, (funcomp (var_vl (S nty) (nvl)) (upRen_ty_vl xi)) x = (up_ty_vl sigma) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition rinstInst_up_vl_ty { m : nat } { nty : nat } (xi : fin (m) → fin (nty)) (sigma : fin (m) → ty (nty)) (Eq : ∀ x, (funcomp (var_ty (nty)) xi) x = sigma x) : ∀ x, (funcomp (var_ty (nty)) (upRen_vl_ty xi)) x = (up_vl_ty sigma) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition rinstInst_up_vl_vl { m : nat } { nty nvl : nat } (xi : fin (m) → fin (nvl)) (sigma : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, (funcomp (var_vl (nty) (nvl)) xi) x = sigma x) : ∀ x, (funcomp (var_vl (nty) (S nvl)) (upRen_vl_vl xi)) x = (up_vl_vl sigma) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint rinst_inst_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (Eqvl : ∀ x, (funcomp (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = subst_tm sigmaty sigmavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s0) (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s0) (rinst_inst_ty xity sigmaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (rinst_inst_vl xity xivl sigmaty sigmavl Eqty Eqvl s0)
end
with rinst_inst_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (Eqvl : ∀ x, (funcomp (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = subst_vl sigmaty sigmavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (rinst_inst_ty xity sigmaty Eqty s0) (rinst_inst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty sigmaty) (up_vl_vl sigmavl) (rinstInst_up_vl_ty (_) (_) Eqty) (rinstInst_up_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (rinst_inst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty sigmaty) (up_ty_vl sigmavl) (rinstInst_up_ty_ty (_) (_) Eqty) (rinstInst_up_ty_vl (_) (_) Eqvl) s0)
end.
Lemma rinstInst_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : ren_tm xity xivl = subst_tm (funcomp (var_ty (nty)) xity) (funcomp (var_vl (nty) (nvl)) xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_tm xity xivl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) x)). Qed.
Lemma rinstInst_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : ren_vl xity xivl = subst_vl (funcomp (var_ty (nty)) xity) (funcomp (var_vl (nty) (nvl)) xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_vl xity xivl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) x)). Qed.
Lemma instId_tm { mty mvl : nat } : subst_tm (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_tm (var_ty (mty)) (var_vl (mty) (mvl)) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma instId_vl { mty mvl : nat } : subst_vl (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_vl (var_ty (mty)) (var_vl (mty) (mvl)) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma rinstId_tm { mty mvl : nat } : @ren_tm (mty) (mvl) (mty) (mvl) id id = id .
Proof. exact (eq_trans (rinstInst_tm id id) instId_tm). Qed.
Lemma rinstId_vl { mty mvl : nat } : @ren_vl (mty) (mvl) (mty) (mvl) id id = id .
Proof. exact (eq_trans (rinstInst_vl id id) instId_vl). Qed.
Lemma varL_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) : funcomp (subst_vl sigmaty sigmavl) (var_vl (mty) (mvl)) = sigmavl .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma varLRen_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : funcomp (ren_vl xity xivl) (var_vl (mty) (mvl)) = funcomp (var_vl (nty) (nvl)) xivl .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma compComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_tm sigmaty sigmavl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_vl sigmaty sigmavl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_tm tauty tauvl) (subst_tm sigmaty sigmavl) = subst_tm (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_tm sigmaty sigmavl tauty tauvl n)). Qed.
Lemma compComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_vl tauty tauvl) (subst_vl sigmaty sigmavl) = subst_vl (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_vl sigmaty sigmavl tauty tauvl n)). Qed.
Lemma compRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen__tm sigmaty sigmavl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen__vl sigmaty sigmavl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_tm zetaty zetavl) (subst_tm sigmaty sigmavl) = subst_tm (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_tm sigmaty sigmavl zetaty zetavl n)). Qed.
Lemma compRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_vl zetaty zetavl) (subst_vl sigmaty sigmavl) = subst_vl (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_vl sigmaty sigmavl zetaty zetavl n)). Qed.
Lemma renComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm (funcomp tauty xity) (funcomp tauvl xivl) s .
Proof. exact (compRenSubst_tm xity xivl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl (funcomp tauty xity) (funcomp tauvl xivl) s .
Proof. exact (compRenSubst_vl xity xivl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_tm tauty tauvl) (ren_tm xity xivl) = subst_tm (funcomp tauty xity) (funcomp tauvl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_tm xity xivl tauty tauvl n)). Qed.
Lemma renComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_vl tauty tauvl) (ren_vl xity xivl) = subst_vl (funcomp tauty xity) (funcomp tauvl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_vl xity xivl tauty tauvl n)). Qed.
Lemma renRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm (funcomp zetaty xity) (funcomp zetavl xivl) s .
Proof. exact (compRenRen_tm xity xivl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl (funcomp zetaty xity) (funcomp zetavl xivl) s .
Proof. exact (compRenRen_vl xity xivl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_tm zetaty zetavl) (ren_tm xity xivl) = ren_tm (funcomp zetaty xity) (funcomp zetavl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_tm xity xivl zetaty zetavl n)). Qed.
Lemma renRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_vl zetaty zetavl) (ren_vl xity xivl) = ren_vl (funcomp zetaty xity) (funcomp zetavl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_vl xity xivl zetaty zetavl n)). Qed.
Arguments var_ty {nty}.
Arguments arr {nty}.
Arguments all {nty}.
Arguments app {nty} {nvl}.
Arguments tapp {nty} {nvl}.
Arguments vt {nty} {nvl}.
Arguments var_vl {nty} {nvl}.
Arguments lam {nty} {nvl}.
Arguments tlam {nty} {nvl}.
Instance Subst_ty { mty : nat } { nty : nat } : Subst1 (fin (mty) → ty (nty)) (ty (mty)) (ty (nty)) := @subst_ty (mty) (nty) .
Instance Subst_tm { mty mvl : nat } { nty nvl : nat } : Subst2 (fin (mty) → ty (nty)) (fin (mvl) → vl (nty) (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @subst_tm (mty) (mvl) (nty) (nvl) .
Instance Subst_vl { mty mvl : nat } { nty nvl : nat } : Subst2 (fin (mty) → ty (nty)) (fin (mvl) → vl (nty) (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @subst_vl (mty) (mvl) (nty) (nvl) .
Instance Ren_ty { mty : nat } { nty : nat } : Ren1 (fin (mty) → fin (nty)) (ty (mty)) (ty (nty)) := @ren_ty (mty) (nty) .
Instance Ren_tm { mty mvl : nat } { nty nvl : nat } : Ren2 (fin (mty) → fin (nty)) (fin (mvl) → fin (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @ren_tm (mty) (mvl) (nty) (nvl) .
Instance Ren_vl { mty mvl : nat } { nty nvl : nat } : Ren2 (fin (mty) → fin (nty)) (fin (mvl) → fin (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @ren_vl (mty) (mvl) (nty) (nvl) .
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_vl { mty mvl : nat } : Var (fin (mvl)) (vl (mty) (mvl)) := @var_vl (mty) (mvl) .
Notation "x '__vl'" := (var_vl x) (at level 5, format "x __vl") : subst_scope.
Notation "x '__vl'" := (@ids (_) (_) VarInstance_vl x) (at level 5, only printing, format "x __vl") : subst_scope.
Notation "'var'" := (var_vl) (only printing, at level 1) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_vl) (only printing) : subst_scope.
Notation "⇑__vl" := (up_vl_ty) (only printing) : subst_scope.
Notation "⇑__vl" := (up_vl_vl) (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 ; sigmavl ]" := (subst_tm sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "s ⟨ xity ; xivl ⟩" := (ren_tm xity xivl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmaty ; sigmavl ]" := (subst_tm sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.
Notation "⟨ xity ; xivl ⟩" := (ren_tm xity xivl) (at level 1, left associativity, only printing) : fscope.
Notation "s [ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "s ⟨ xity ; xivl ⟩" := (ren_vl xity xivl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.
Notation "⟨ xity ; xivl ⟩" := (ren_vl xity xivl) (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, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Subst_ty, Subst_tm, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl in ×.
Ltac asimpl' := repeat first [progress rewrite ?instId_ty| progress rewrite ?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 ?instId_vl| progress rewrite ?rinstId_vl| progress rewrite ?compComp_vl| progress rewrite ?compComp'_vl| progress rewrite ?compRen_vl| progress rewrite ?compRen'_vl| progress rewrite ?renComp_vl| progress rewrite ?renComp'_vl| progress rewrite ?renRen_vl| progress rewrite ?renRen'_vl| progress rewrite ?varL_ty| progress rewrite ?varLRen_ty| progress rewrite ?varL_vl| progress rewrite ?varLRen_vl| progress (unfold up_ren, upRen_ty_ty, upRen_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, up_ty_ty, up_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_ty in *| progress rewrite ?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 ?instId_vl in *| progress rewrite ?rinstId_vl in *| progress rewrite ?compComp_vl in *| progress rewrite ?compComp'_vl in *| progress rewrite ?compRen_vl in *| progress rewrite ?compRen'_vl in *| progress rewrite ?renComp_vl in *| progress rewrite ?renComp'_vl in *| progress rewrite ?renRen_vl in *| progress rewrite ?renRen'_vl in *| progress rewrite ?varL_ty in *| progress rewrite ?varLRen_ty in *| progress rewrite ?varL_vl in *| progress rewrite ?varLRen_vl in *| progress (unfold up_ren, upRen_ty_ty, upRen_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, up_ty_ty, up_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl in *)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl] in *)| fsimpl in *].
Ltac substify := auto_unfold; try repeat (erewrite rinst_inst_ty; [|now intros]); try repeat (erewrite rinst_inst_tm; [|now intros]); try repeat (erewrite rinst_inst_vl; [|now intros]).
Ltac renamify := auto_unfold; try repeat (erewrite <- rinst_inst_ty; [|intros; now asimpl]); try repeat (erewrite <- rinst_inst_tm; [|intros; now asimpl]); try repeat (erewrite <- rinst_inst_vl; [|intros; now asimpl]).
Inductive ty (nty : nat) : Type :=
| var_ty : fin (nty) → ty (nty)
| arr : ty (nty) → ty (nty) → ty (nty)
| all : ty (S nty) → ty (nty).
Lemma congr_arr { mty : nat } { s0 : ty (mty) } { s1 : ty (mty) } { t0 : ty (mty) } { t1 : ty (mty) } : s0 = t0 → s1 = t1 → arr (mty) s0 s1 = arr (mty) t0 t1 .
Proof. congruence. Qed.
Lemma congr_all { mty : nat } { s0 : ty (S mty) } { t0 : ty (S mty) } : s0 = t0 → all (mty) s0 = all (mty) t0 .
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)
| arr (_) s0 s1 ⇒ arr (nty) (ren_ty xity s0) (ren_ty xity s1)
| all (_) s0 ⇒ all (nty) (ren_ty (upRen_ty_ty xity) s0)
end.
Definition up_ty_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) : _ :=
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
| arr (_) s0 s1 ⇒ arr (nty) (subst_ty sigmaty s0) (subst_ty sigmaty s1)
| all (_) s0 ⇒ all (nty) (subst_ty (up_ty_ty sigmaty) s0)
end.
Definition upId_ty_ty { mty : nat } (sigma : fin (mty) → ty (mty)) (Eq : ∀ x, sigma x = (var_ty (mty)) x) : ∀ 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 : ∀ x, sigmaty x = (var_ty (mty)) x) (s : ty (mty)) : subst_ty sigmaty s = s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (idSubst_ty sigmaty Eqty s0) (idSubst_ty sigmaty Eqty s1)
| all (_) s0 ⇒ congr_all (idSubst_ty (up_ty_ty sigmaty) (upId_ty_ty (_) Eqty) s0)
end.
Definition upExtRen_ty_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ 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 : ∀ x, xity x = zetaty x) (s : ty (mty)) : ren_ty xity s = ren_ty zetaty s :=
match s with
| var_ty (_) s ⇒ ap (var_ty (nty)) (Eqty s)
| arr (_) s0 s1 ⇒ congr_arr (extRen_ty xity zetaty Eqty s0) (extRen_ty xity zetaty Eqty s1)
| all (_) s0 ⇒ congr_all (extRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upExtRen_ty_ty (_) (_) Eqty) s0)
end.
Definition upExt_ty_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) (tau : fin (m) → ty (nty)) (Eq : ∀ x, sigma x = tau x) : ∀ 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 : ∀ x, sigmaty x = tauty x) (s : ty (mty)) : subst_ty sigmaty s = subst_ty tauty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (ext_ty sigmaty tauty Eqty s0) (ext_ty sigmaty tauty Eqty s1)
| all (_) s0 ⇒ congr_all (ext_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (upExt_ty_ty (_) (_) Eqty) s0)
end.
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 : ∀ x, (funcomp zetaty xity) x = rhoty x) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty rhoty s :=
match s with
| var_ty (_) s ⇒ ap (var_ty (lty)) (Eqty s)
| arr (_) s0 s1 ⇒ congr_arr (compRenRen_ty xity zetaty rhoty Eqty s0) (compRenRen_ty xity zetaty rhoty Eqty s1)
| all (_) s0 ⇒ congr_all (compRenRen_ty (upRen_ty_ty xity) (upRen_ty_ty zetaty) (upRen_ty_ty rhoty) (up_ren_ren (_) (_) (_) Eqty) s0)
end.
Definition up_ren_subst_ty_ty { k : nat } { l : nat } { mty : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ 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 : ∀ x, (funcomp tauty xity) x = thetaty x) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compRenSubst_ty xity tauty thetaty Eqty s0) (compRenSubst_ty xity tauty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compRenSubst_ty (upRen_ty_ty xity) (up_ty_ty tauty) (up_ty_ty thetaty) (up_ren_subst_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition up_subst_ren_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (zetaty : fin (lty) → fin (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (ren_ty zetaty) sigma) x = theta x) : ∀ 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 : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compSubstRen__ty sigmaty zetaty thetaty Eqty s0) (compSubstRen__ty sigmaty zetaty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compSubstRen__ty (up_ty_ty sigmaty) (upRen_ty_ty zetaty) (up_ty_ty thetaty) (up_subst_ren_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition up_subst_subst_ty_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (tauty : fin (lty) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (subst_ty tauty) sigma) x = theta x) : ∀ 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 : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty thetaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (compSubstSubst_ty sigmaty tauty thetaty Eqty s0) (compSubstSubst_ty sigmaty tauty thetaty Eqty s1)
| all (_) s0 ⇒ congr_all (compSubstSubst_ty (up_ty_ty sigmaty) (up_ty_ty tauty) (up_ty_ty thetaty) (up_subst_subst_ty_ty (_) (_) (_) Eqty) s0)
end.
Definition rinstInst_up_ty_ty { m : nat } { nty : nat } (xi : fin (m) → fin (nty)) (sigma : fin (m) → ty (nty)) (Eq : ∀ x, (funcomp (var_ty (nty)) xi) x = sigma x) : ∀ 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 : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (s : ty (mty)) : ren_ty xity s = subst_ty sigmaty s :=
match s with
| var_ty (_) s ⇒ Eqty s
| arr (_) s0 s1 ⇒ congr_arr (rinst_inst_ty xity sigmaty Eqty s0) (rinst_inst_ty xity sigmaty Eqty s1)
| all (_) s0 ⇒ congr_all (rinst_inst_ty (upRen_ty_ty xity) (up_ty_ty sigmaty) (rinstInst_up_ty_ty (_) (_) Eqty) s0)
end.
Lemma rinstInst_ty { mty : nat } { nty : nat } (xity : fin (mty) → fin (nty)) : ren_ty xity = subst_ty (funcomp (var_ty (nty)) xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_ty xity (_) (fun n ⇒ eq_refl) x)). Qed.
Lemma instId_ty { mty : nat } : subst_ty (var_ty (mty)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_ty (var_ty (mty)) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma rinstId_ty { mty : nat } : @ren_ty (mty) (mty) id = id .
Proof. exact (eq_trans (rinstInst_ty id) instId_ty). Qed.
Lemma varL_ty { mty : nat } { nty : nat } (sigmaty : fin (mty) → ty (nty)) : funcomp (subst_ty sigmaty) (var_ty (mty)) = sigmaty .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma varLRen_ty { mty : nat } { nty : nat } (xity : fin (mty) → fin (nty)) : funcomp (ren_ty xity) (var_ty (mty)) = funcomp (var_ty (nty)) xity .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma compComp_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (tauty : fin (kty) → ty (lty)) (s : ty (mty)) : subst_ty tauty (subst_ty sigmaty s) = subst_ty (funcomp (subst_ty tauty) sigmaty) s .
Proof. exact (compSubstSubst_ty sigmaty tauty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (tauty : fin (kty) → ty (lty)) : funcomp (subst_ty tauty) (subst_ty sigmaty) = subst_ty (funcomp (subst_ty tauty) sigmaty) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_ty sigmaty tauty n)). Qed.
Lemma compRen_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (zetaty : fin (kty) → fin (lty)) (s : ty (mty)) : ren_ty zetaty (subst_ty sigmaty s) = subst_ty (funcomp (ren_ty zetaty) sigmaty) s .
Proof. exact (compSubstRen__ty sigmaty zetaty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen'_ty { kty : nat } { lty : nat } { mty : nat } (sigmaty : fin (mty) → ty (kty)) (zetaty : fin (kty) → fin (lty)) : funcomp (ren_ty zetaty) (subst_ty sigmaty) = subst_ty (funcomp (ren_ty zetaty) sigmaty) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_ty sigmaty zetaty n)). Qed.
Lemma renComp_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (tauty : fin (kty) → ty (lty)) (s : ty (mty)) : subst_ty tauty (ren_ty xity s) = subst_ty (funcomp tauty xity) s .
Proof. exact (compRenSubst_ty xity tauty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp'_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (tauty : fin (kty) → ty (lty)) : funcomp (subst_ty tauty) (ren_ty xity) = subst_ty (funcomp tauty xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_ty xity tauty n)). Qed.
Lemma renRen_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (zetaty : fin (kty) → fin (lty)) (s : ty (mty)) : ren_ty zetaty (ren_ty xity s) = ren_ty (funcomp zetaty xity) s .
Proof. exact (compRenRen_ty xity zetaty (_) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen'_ty { kty : nat } { lty : nat } { mty : nat } (xity : fin (mty) → fin (kty)) (zetaty : fin (kty) → fin (lty)) : funcomp (ren_ty zetaty) (ren_ty xity) = ren_ty (funcomp zetaty xity) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_ty xity zetaty n)). Qed.
Inductive tm (nty nvl : nat) : Type :=
| app : tm (nty) (nvl) → tm (nty) (nvl) → tm (nty) (nvl)
| tapp : tm (nty) (nvl) → ty (nty) → tm (nty) (nvl)
| vt : vl (nty) (nvl) → tm (nty) (nvl)
with vl (nty nvl : nat) : Type :=
| var_vl : fin (nvl) → vl (nty) (nvl)
| lam : ty (nty) → tm (nty) (S nvl) → vl (nty) (nvl)
| tlam : tm (S nty) (nvl) → vl (nty) (nvl).
Lemma congr_app { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : tm (mty) (mvl) } { t0 : tm (mty) (mvl) } { t1 : tm (mty) (mvl) } : s0 = t0 → s1 = t1 → app (mty) (mvl) s0 s1 = app (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tapp { mty mvl : nat } { s0 : tm (mty) (mvl) } { s1 : ty (mty) } { t0 : tm (mty) (mvl) } { t1 : ty (mty) } : s0 = t0 → s1 = t1 → tapp (mty) (mvl) s0 s1 = tapp (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_vt { mty mvl : nat } { s0 : vl (mty) (mvl) } { t0 : vl (mty) (mvl) } : s0 = t0 → vt (mty) (mvl) s0 = vt (mty) (mvl) t0 .
Proof. congruence. Qed.
Lemma congr_lam { mty mvl : nat } { s0 : ty (mty) } { s1 : tm (mty) (S mvl) } { t0 : ty (mty) } { t1 : tm (mty) (S mvl) } : s0 = t0 → s1 = t1 → lam (mty) (mvl) s0 s1 = lam (mty) (mvl) t0 t1 .
Proof. congruence. Qed.
Lemma congr_tlam { mty mvl : nat } { s0 : tm (S mty) (mvl) } { t0 : tm (S mty) (mvl) } : s0 = t0 → tlam (mty) (mvl) s0 = tlam (mty) (mvl) t0 .
Proof. congruence. Qed.
Definition upRen_ty_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
xi.
Definition upRen_vl_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
xi.
Definition upRen_vl_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) : _ :=
up_ren xi.
Fixpoint ren_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (s : tm (mty) (mvl)) : _ :=
match s with
| app (_) (_) s0 s1 ⇒ app (nty) (nvl) (ren_tm xity xivl s0) (ren_tm xity xivl s1)
| tapp (_) (_) s0 s1 ⇒ tapp (nty) (nvl) (ren_tm xity xivl s0) (ren_ty xity s1)
| vt (_) (_) s0 ⇒ vt (nty) (nvl) (ren_vl xity xivl s0)
end
with ren_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (s : vl (mty) (mvl)) : _ :=
match s with
| var_vl (_) (_) s ⇒ (var_vl (nty) (nvl)) (xivl s)
| lam (_) (_) s0 s1 ⇒ lam (nty) (nvl) (ren_ty xity s0) (ren_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) s1)
| tlam (_) (_) s0 ⇒ tlam (nty) (nvl) (ren_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) s0)
end.
Definition up_ty_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) : _ :=
funcomp (ren_vl shift id) sigma.
Definition up_vl_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) : _ :=
funcomp (ren_ty id) sigma.
Definition up_vl_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) : _ :=
scons ((var_vl (nty) (S nvl)) var_zero) (funcomp (ren_vl id shift) sigma).
Fixpoint subst_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (s : tm (mty) (mvl)) : _ :=
match s with
| app (_) (_) s0 s1 ⇒ app (nty) (nvl) (subst_tm sigmaty sigmavl s0) (subst_tm sigmaty sigmavl s1)
| tapp (_) (_) s0 s1 ⇒ tapp (nty) (nvl) (subst_tm sigmaty sigmavl s0) (subst_ty sigmaty s1)
| vt (_) (_) s0 ⇒ vt (nty) (nvl) (subst_vl sigmaty sigmavl s0)
end
with subst_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (s : vl (mty) (mvl)) : _ :=
match s with
| var_vl (_) (_) s ⇒ sigmavl s
| lam (_) (_) s0 s1 ⇒ lam (nty) (nvl) (subst_ty sigmaty s0) (subst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) s1)
| tlam (_) (_) s0 ⇒ tlam (nty) (nvl) (subst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) s0)
end.
Definition upId_ty_vl { mty mvl : nat } (sigma : fin (mvl) → vl (mty) (mvl)) (Eq : ∀ x, sigma x = (var_vl (mty) (mvl)) x) : ∀ x, (up_ty_vl sigma) x = (var_vl (S mty) (mvl)) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition upId_vl_ty { mty : nat } (sigma : fin (mty) → ty (mty)) (Eq : ∀ x, sigma x = (var_ty (mty)) x) : ∀ x, (up_vl_ty sigma) x = (var_ty (mty)) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition upId_vl_vl { mty mvl : nat } (sigma : fin (mvl) → vl (mty) (mvl)) (Eq : ∀ x, sigma x = (var_vl (mty) (mvl)) x) : ∀ x, (up_vl_vl sigma) x = (var_vl (mty) (S mvl)) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint idSubst_tm { mty mvl : nat } (sigmaty : fin (mty) → ty (mty)) (sigmavl : fin (mvl) → vl (mty) (mvl)) (Eqty : ∀ x, sigmaty x = (var_ty (mty)) x) (Eqvl : ∀ x, sigmavl x = (var_vl (mty) (mvl)) x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (idSubst_tm sigmaty sigmavl Eqty Eqvl s0) (idSubst_tm sigmaty sigmavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (idSubst_tm sigmaty sigmavl Eqty Eqvl s0) (idSubst_ty sigmaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (idSubst_vl sigmaty sigmavl Eqty Eqvl s0)
end
with idSubst_vl { mty mvl : nat } (sigmaty : fin (mty) → ty (mty)) (sigmavl : fin (mvl) → vl (mty) (mvl)) (Eqty : ∀ x, sigmaty x = (var_ty (mty)) x) (Eqvl : ∀ x, sigmavl x = (var_vl (mty) (mvl)) x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (idSubst_ty sigmaty Eqty s0) (idSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upId_vl_ty (_) Eqty) (upId_vl_vl (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (idSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upId_ty_ty (_) Eqty) (upId_ty_vl (_) Eqvl) s0)
end.
Definition upExtRen_ty_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_ty_vl xi) x = (upRen_ty_vl zeta) x :=
fun n ⇒ Eq n.
Definition upExtRen_vl_ty { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_vl_ty xi) x = (upRen_vl_ty zeta) x :=
fun n ⇒ Eq n.
Definition upExtRen_vl_vl { m : nat } { n : nat } (xi : fin (m) → fin (n)) (zeta : fin (m) → fin (n)) (Eq : ∀ x, xi x = zeta x) : ∀ x, (upRen_vl_vl xi) x = (upRen_vl_vl zeta) x :=
fun n ⇒ match n with
| Some n ⇒ ap shift (Eq n)
| None ⇒ eq_refl
end.
Fixpoint extRen_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (zetaty : fin (mty) → fin (nty)) (zetavl : fin (mvl) → fin (nvl)) (Eqty : ∀ x, xity x = zetaty x) (Eqvl : ∀ x, xivl x = zetavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = ren_tm zetaty zetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s0) (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (extRen_tm xity xivl zetaty zetavl Eqty Eqvl s0) (extRen_ty xity zetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (extRen_vl xity xivl zetaty zetavl Eqty Eqvl s0)
end
with extRen_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (zetaty : fin (mty) → fin (nty)) (zetavl : fin (mvl) → fin (nvl)) (Eqty : ∀ x, xity x = zetaty x) (Eqvl : ∀ x, xivl x = zetavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = ren_vl zetaty zetavl s :=
match s with
| var_vl (_) (_) s ⇒ ap (var_vl (nty) (nvl)) (Eqvl s)
| lam (_) (_) s0 s1 ⇒ congr_lam (extRen_ty xity zetaty Eqty s0) (extRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upExtRen_vl_ty (_) (_) Eqty) (upExtRen_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (extRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upExtRen_ty_ty (_) (_) Eqty) (upExtRen_ty_vl (_) (_) Eqvl) s0)
end.
Definition upExt_ty_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) (tau : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_ty_vl sigma) x = (up_ty_vl tau) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition upExt_vl_ty { m : nat } { nty : nat } (sigma : fin (m) → ty (nty)) (tau : fin (m) → ty (nty)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_vl_ty sigma) x = (up_vl_ty tau) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition upExt_vl_vl { m : nat } { nty nvl : nat } (sigma : fin (m) → vl (nty) (nvl)) (tau : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, sigma x = tau x) : ∀ x, (up_vl_vl sigma) x = (up_vl_vl tau) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint ext_tm { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (tauty : fin (mty) → ty (nty)) (tauvl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, sigmaty x = tauty x) (Eqvl : ∀ x, sigmavl x = tauvl x) (s : tm (mty) (mvl)) : subst_tm sigmaty sigmavl s = subst_tm tauty tauvl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s0) (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (ext_tm sigmaty sigmavl tauty tauvl Eqty Eqvl s0) (ext_ty sigmaty tauty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (ext_vl sigmaty sigmavl tauty tauvl Eqty Eqvl s0)
end
with ext_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (tauty : fin (mty) → ty (nty)) (tauvl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, sigmaty x = tauty x) (Eqvl : ∀ x, sigmavl x = tauvl x) (s : vl (mty) (mvl)) : subst_vl sigmaty sigmavl s = subst_vl tauty tauvl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (ext_ty sigmaty tauty Eqty s0) (ext_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (upExt_vl_ty (_) (_) Eqty) (upExt_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (ext_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (upExt_ty_ty (_) (_) Eqty) (upExt_ty_vl (_) (_) Eqvl) s0)
end.
Fixpoint compRenRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (rhoty : fin (mty) → fin (lty)) (rhovl : fin (mvl) → fin (lvl)) (Eqty : ∀ x, (funcomp zetaty xity) x = rhoty x) (Eqvl : ∀ x, (funcomp zetavl xivl) x = rhovl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm rhoty rhovl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0) (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compRenRen_tm xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0) (compRenRen_ty xity zetaty rhoty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compRenRen_vl xity xivl zetaty zetavl rhoty rhovl Eqty Eqvl s0)
end
with compRenRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (rhoty : fin (mty) → fin (lty)) (rhovl : fin (mvl) → fin (lvl)) (Eqty : ∀ x, (funcomp zetaty xity) x = rhoty x) (Eqvl : ∀ x, (funcomp zetavl xivl) x = rhovl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl rhoty rhovl s :=
match s with
| var_vl (_) (_) s ⇒ ap (var_vl (lty) (lvl)) (Eqvl s)
| lam (_) (_) s0 s1 ⇒ congr_lam (compRenRen_ty xity zetaty rhoty Eqty s0) (compRenRen_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (upRen_vl_ty rhoty) (upRen_vl_vl rhovl) Eqty (up_ren_ren (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compRenRen_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (upRen_ty_ty rhoty) (upRen_ty_vl rhovl) (up_ren_ren (_) (_) (_) Eqty) Eqvl s0)
end.
Definition up_ren_subst_ty_vl { k : nat } { l : nat } { mty mvl : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_ty_vl tau) (upRen_ty_vl xi)) x = (up_ty_vl theta) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition up_ren_subst_vl_ty { k : nat } { l : nat } { mty : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_vl_ty tau) (upRen_vl_ty xi)) x = (up_vl_ty theta) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition up_ren_subst_vl_vl { k : nat } { l : nat } { mty mvl : nat } (xi : fin (k) → fin (l)) (tau : fin (l) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp tau xi) x = theta x) : ∀ x, (funcomp (up_vl_vl tau) (upRen_vl_vl xi)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint compRenSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp tauty xity) x = thetaty x) (Eqvl : ∀ x, (funcomp tauvl xivl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compRenSubst_tm xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compRenSubst_ty xity tauty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compRenSubst_vl xity xivl tauty tauvl thetaty thetavl Eqty Eqvl s0)
end
with compRenSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp tauty xity) x = thetaty x) (Eqvl : ∀ x, (funcomp tauvl xivl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compRenSubst_ty xity tauty thetaty Eqty s0) (compRenSubst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_ren_subst_vl_ty (_) (_) (_) Eqty) (up_ren_subst_vl_vl (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compRenSubst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_ren_subst_ty_ty (_) (_) (_) Eqty) (up_ren_subst_ty_vl (_) (_) (_) Eqvl) s0)
end.
Definition up_subst_ren_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (zetaty : fin (lty) → fin (mty)) (zetavl : fin (lvl) → fin (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (ren_vl zetaty zetavl) sigma) x = theta x) : ∀ x, (funcomp (ren_vl (upRen_ty_ty zetaty) (upRen_ty_vl zetavl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
fun n ⇒ eq_trans (compRenRen_vl shift id (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (funcomp shift zetaty) (funcomp id zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_vl zetaty zetavl shift id (funcomp shift zetaty) (funcomp id zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl shift id) (Eq n))).
Definition up_subst_ren_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (zetaty : fin (lty) → fin (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (ren_ty zetaty) sigma) x = theta x) : ∀ x, (funcomp (ren_ty (upRen_vl_ty zetaty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
fun n ⇒ eq_trans (compRenRen_ty id (upRen_vl_ty zetaty) (funcomp id zetaty) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_ty zetaty id (funcomp id zetaty) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_ty id) (Eq n))).
Definition up_subst_ren_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (zetaty : fin (lty) → fin (mty)) (zetavl : fin (lvl) → fin (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (ren_vl zetaty zetavl) sigma) x = theta x) : ∀ x, (funcomp (ren_vl (upRen_vl_ty zetaty) (upRen_vl_vl zetavl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ eq_trans (compRenRen_vl id shift (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (funcomp id zetaty) (funcomp shift zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_vl zetaty zetavl id shift (funcomp id zetaty) (funcomp shift zetavl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl id shift) (Eq n)))
| None ⇒ eq_refl
end.
Fixpoint compSubstRen__tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0) (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compSubstRen__tm sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0) (compSubstRen__ty sigmaty zetaty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compSubstRen__vl sigmaty sigmavl zetaty zetavl thetaty thetavl Eqty Eqvl s0)
end
with compSubstRen__vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (ren_ty zetaty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (ren_vl zetaty zetavl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compSubstRen__ty sigmaty zetaty thetaty Eqty s0) (compSubstRen__tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (upRen_vl_ty zetaty) (upRen_vl_vl zetavl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_ren_vl_ty (_) (_) (_) Eqty) (up_subst_ren_vl_vl (_) (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compSubstRen__tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (upRen_ty_ty zetaty) (upRen_ty_vl zetavl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_ren_ty_ty (_) (_) (_) Eqty) (up_subst_ren_ty_vl (_) (_) (_) (_) Eqvl) s0)
end.
Definition up_subst_subst_ty_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (tauty : fin (lty) → ty (mty)) (tauvl : fin (lvl) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (subst_vl tauty tauvl) sigma) x = theta x) : ∀ x, (funcomp (subst_vl (up_ty_ty tauty) (up_ty_vl tauvl)) (up_ty_vl sigma)) x = (up_ty_vl theta) x :=
fun n ⇒ eq_trans (compRenSubst_vl shift id (up_ty_ty tauty) (up_ty_vl tauvl) (funcomp (up_ty_ty tauty) shift) (funcomp (up_ty_vl tauvl) id) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__vl tauty tauvl shift id (funcomp (ren_ty shift) tauty) (funcomp (ren_vl shift id) tauvl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl shift id) (Eq n))).
Definition up_subst_subst_vl_ty { k : nat } { lty : nat } { mty : nat } (sigma : fin (k) → ty (lty)) (tauty : fin (lty) → ty (mty)) (theta : fin (k) → ty (mty)) (Eq : ∀ x, (funcomp (subst_ty tauty) sigma) x = theta x) : ∀ x, (funcomp (subst_ty (up_vl_ty tauty)) (up_vl_ty sigma)) x = (up_vl_ty theta) x :=
fun n ⇒ eq_trans (compRenSubst_ty id (up_vl_ty tauty) (funcomp (up_vl_ty tauty) id) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__ty tauty id (funcomp (ren_ty id) tauty) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_ty id) (Eq n))).
Definition up_subst_subst_vl_vl { k : nat } { lty lvl : nat } { mty mvl : nat } (sigma : fin (k) → vl (lty) (lvl)) (tauty : fin (lty) → ty (mty)) (tauvl : fin (lvl) → vl (mty) (mvl)) (theta : fin (k) → vl (mty) (mvl)) (Eq : ∀ x, (funcomp (subst_vl tauty tauvl) sigma) x = theta x) : ∀ x, (funcomp (subst_vl (up_vl_ty tauty) (up_vl_vl tauvl)) (up_vl_vl sigma)) x = (up_vl_vl theta) x :=
fun n ⇒ match n with
| Some n ⇒ eq_trans (compRenSubst_vl id shift (up_vl_ty tauty) (up_vl_vl tauvl) (funcomp (up_vl_ty tauty) id) (funcomp (up_vl_vl tauvl) shift) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__vl tauty tauvl id shift (funcomp (ren_ty id) tauty) (funcomp (ren_vl id shift) tauvl) (fun x ⇒ eq_refl) (fun x ⇒ eq_refl) (sigma n))) (ap (ren_vl id shift) (Eq n)))
| None ⇒ eq_refl
end.
Fixpoint compSubstSubst_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm thetaty thetavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (compSubstSubst_tm sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0) (compSubstSubst_ty sigmaty tauty thetaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (compSubstSubst_vl sigmaty sigmavl tauty tauvl thetaty thetavl Eqty Eqvl s0)
end
with compSubstSubst_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (thetaty : fin (mty) → ty (lty)) (thetavl : fin (mvl) → vl (lty) (lvl)) (Eqty : ∀ x, (funcomp (subst_ty tauty) sigmaty) x = thetaty x) (Eqvl : ∀ x, (funcomp (subst_vl tauty tauvl) sigmavl) x = thetavl x) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl thetaty thetavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (compSubstSubst_ty sigmaty tauty thetaty Eqty s0) (compSubstSubst_tm (up_vl_ty sigmaty) (up_vl_vl sigmavl) (up_vl_ty tauty) (up_vl_vl tauvl) (up_vl_ty thetaty) (up_vl_vl thetavl) (up_subst_subst_vl_ty (_) (_) (_) Eqty) (up_subst_subst_vl_vl (_) (_) (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (compSubstSubst_tm (up_ty_ty sigmaty) (up_ty_vl sigmavl) (up_ty_ty tauty) (up_ty_vl tauvl) (up_ty_ty thetaty) (up_ty_vl thetavl) (up_subst_subst_ty_ty (_) (_) (_) Eqty) (up_subst_subst_ty_vl (_) (_) (_) (_) Eqvl) s0)
end.
Definition rinstInst_up_ty_vl { m : nat } { nty nvl : nat } (xi : fin (m) → fin (nvl)) (sigma : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, (funcomp (var_vl (nty) (nvl)) xi) x = sigma x) : ∀ x, (funcomp (var_vl (S nty) (nvl)) (upRen_ty_vl xi)) x = (up_ty_vl sigma) x :=
fun n ⇒ ap (ren_vl shift id) (Eq n).
Definition rinstInst_up_vl_ty { m : nat } { nty : nat } (xi : fin (m) → fin (nty)) (sigma : fin (m) → ty (nty)) (Eq : ∀ x, (funcomp (var_ty (nty)) xi) x = sigma x) : ∀ x, (funcomp (var_ty (nty)) (upRen_vl_ty xi)) x = (up_vl_ty sigma) x :=
fun n ⇒ ap (ren_ty id) (Eq n).
Definition rinstInst_up_vl_vl { m : nat } { nty nvl : nat } (xi : fin (m) → fin (nvl)) (sigma : fin (m) → vl (nty) (nvl)) (Eq : ∀ x, (funcomp (var_vl (nty) (nvl)) xi) x = sigma x) : ∀ x, (funcomp (var_vl (nty) (S nvl)) (upRen_vl_vl xi)) x = (up_vl_vl sigma) x :=
fun n ⇒ match n with
| Some n ⇒ ap (ren_vl id shift) (Eq n)
| None ⇒ eq_refl
end.
Fixpoint rinst_inst_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (Eqvl : ∀ x, (funcomp (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : tm (mty) (mvl)) : ren_tm xity xivl s = subst_tm sigmaty sigmavl s :=
match s with
| app (_) (_) s0 s1 ⇒ congr_app (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s0) (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s1)
| tapp (_) (_) s0 s1 ⇒ congr_tapp (rinst_inst_tm xity xivl sigmaty sigmavl Eqty Eqvl s0) (rinst_inst_ty xity sigmaty Eqty s1)
| vt (_) (_) s0 ⇒ congr_vt (rinst_inst_vl xity xivl sigmaty sigmavl Eqty Eqvl s0)
end
with rinst_inst_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) (Eqty : ∀ x, (funcomp (var_ty (nty)) xity) x = sigmaty x) (Eqvl : ∀ x, (funcomp (var_vl (nty) (nvl)) xivl) x = sigmavl x) (s : vl (mty) (mvl)) : ren_vl xity xivl s = subst_vl sigmaty sigmavl s :=
match s with
| var_vl (_) (_) s ⇒ Eqvl s
| lam (_) (_) s0 s1 ⇒ congr_lam (rinst_inst_ty xity sigmaty Eqty s0) (rinst_inst_tm (upRen_vl_ty xity) (upRen_vl_vl xivl) (up_vl_ty sigmaty) (up_vl_vl sigmavl) (rinstInst_up_vl_ty (_) (_) Eqty) (rinstInst_up_vl_vl (_) (_) Eqvl) s1)
| tlam (_) (_) s0 ⇒ congr_tlam (rinst_inst_tm (upRen_ty_ty xity) (upRen_ty_vl xivl) (up_ty_ty sigmaty) (up_ty_vl sigmavl) (rinstInst_up_ty_ty (_) (_) Eqty) (rinstInst_up_ty_vl (_) (_) Eqvl) s0)
end.
Lemma rinstInst_tm { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : ren_tm xity xivl = subst_tm (funcomp (var_ty (nty)) xity) (funcomp (var_vl (nty) (nvl)) xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_tm xity xivl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) x)). Qed.
Lemma rinstInst_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : ren_vl xity xivl = subst_vl (funcomp (var_ty (nty)) xity) (funcomp (var_vl (nty) (nvl)) xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ rinst_inst_vl xity xivl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) x)). Qed.
Lemma instId_tm { mty mvl : nat } : subst_tm (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_tm (var_ty (mty)) (var_vl (mty) (mvl)) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma instId_vl { mty mvl : nat } : subst_vl (var_ty (mty)) (var_vl (mty) (mvl)) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ idSubst_vl (var_ty (mty)) (var_vl (mty) (mvl)) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) (id x))). Qed.
Lemma rinstId_tm { mty mvl : nat } : @ren_tm (mty) (mvl) (mty) (mvl) id id = id .
Proof. exact (eq_trans (rinstInst_tm id id) instId_tm). Qed.
Lemma rinstId_vl { mty mvl : nat } : @ren_vl (mty) (mvl) (mty) (mvl) id id = id .
Proof. exact (eq_trans (rinstInst_vl id id) instId_vl). Qed.
Lemma varL_vl { mty mvl : nat } { nty nvl : nat } (sigmaty : fin (mty) → ty (nty)) (sigmavl : fin (mvl) → vl (nty) (nvl)) : funcomp (subst_vl sigmaty sigmavl) (var_vl (mty) (mvl)) = sigmavl .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma varLRen_vl { mty mvl : nat } { nty nvl : nat } (xity : fin (mty) → fin (nty)) (xivl : fin (mvl) → fin (nvl)) : funcomp (ren_vl xity xivl) (var_vl (mty) (mvl)) = funcomp (var_vl (nty) (nvl)) xivl .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x ⇒ eq_refl)). Qed.
Lemma compComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (subst_tm sigmaty sigmavl s) = subst_tm (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_tm sigmaty sigmavl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (subst_vl sigmaty sigmavl s) = subst_vl (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) s .
Proof. exact (compSubstSubst_vl sigmaty sigmavl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_tm tauty tauvl) (subst_tm sigmaty sigmavl) = subst_tm (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_tm sigmaty sigmavl tauty tauvl n)). Qed.
Lemma compComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_vl tauty tauvl) (subst_vl sigmaty sigmavl) = subst_vl (funcomp (subst_ty tauty) sigmaty) (funcomp (subst_vl tauty tauvl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compComp_vl sigmaty sigmavl tauty tauvl n)). Qed.
Lemma compRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (subst_tm sigmaty sigmavl s) = subst_tm (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen__tm sigmaty sigmavl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (subst_vl sigmaty sigmavl s) = subst_vl (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) s .
Proof. exact (compSubstRen__vl sigmaty sigmavl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma compRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_tm zetaty zetavl) (subst_tm sigmaty sigmavl) = subst_tm (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_tm sigmaty sigmavl zetaty zetavl n)). Qed.
Lemma compRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (sigmaty : fin (mty) → ty (kty)) (sigmavl : fin (mvl) → vl (kty) (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_vl zetaty zetavl) (subst_vl sigmaty sigmavl) = subst_vl (funcomp (ren_ty zetaty) sigmaty) (funcomp (ren_vl zetaty zetavl) sigmavl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ compRen_vl sigmaty sigmavl zetaty zetavl n)). Qed.
Lemma renComp_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : tm (mty) (mvl)) : subst_tm tauty tauvl (ren_tm xity xivl s) = subst_tm (funcomp tauty xity) (funcomp tauvl xivl) s .
Proof. exact (compRenSubst_tm xity xivl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) (s : vl (mty) (mvl)) : subst_vl tauty tauvl (ren_vl xity xivl s) = subst_vl (funcomp tauty xity) (funcomp tauvl xivl) s .
Proof. exact (compRenSubst_vl xity xivl tauty tauvl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renComp'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_tm tauty tauvl) (ren_tm xity xivl) = subst_tm (funcomp tauty xity) (funcomp tauvl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_tm xity xivl tauty tauvl n)). Qed.
Lemma renComp'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (tauty : fin (kty) → ty (lty)) (tauvl : fin (kvl) → vl (lty) (lvl)) : funcomp (subst_vl tauty tauvl) (ren_vl xity xivl) = subst_vl (funcomp tauty xity) (funcomp tauvl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renComp_vl xity xivl tauty tauvl n)). Qed.
Lemma renRen_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : tm (mty) (mvl)) : ren_tm zetaty zetavl (ren_tm xity xivl s) = ren_tm (funcomp zetaty xity) (funcomp zetavl xivl) s .
Proof. exact (compRenRen_tm xity xivl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) (s : vl (mty) (mvl)) : ren_vl zetaty zetavl (ren_vl xity xivl s) = ren_vl (funcomp zetaty xity) (funcomp zetavl xivl) s .
Proof. exact (compRenRen_vl xity xivl zetaty zetavl (_) (_) (fun n ⇒ eq_refl) (fun n ⇒ eq_refl) s). Qed.
Lemma renRen'_tm { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_tm zetaty zetavl) (ren_tm xity xivl) = ren_tm (funcomp zetaty xity) (funcomp zetavl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_tm xity xivl zetaty zetavl n)). Qed.
Lemma renRen'_vl { kty kvl : nat } { lty lvl : nat } { mty mvl : nat } (xity : fin (mty) → fin (kty)) (xivl : fin (mvl) → fin (kvl)) (zetaty : fin (kty) → fin (lty)) (zetavl : fin (kvl) → fin (lvl)) : funcomp (ren_vl zetaty zetavl) (ren_vl xity xivl) = ren_vl (funcomp zetaty xity) (funcomp zetavl xivl) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n ⇒ renRen_vl xity xivl zetaty zetavl n)). Qed.
Arguments var_ty {nty}.
Arguments arr {nty}.
Arguments all {nty}.
Arguments app {nty} {nvl}.
Arguments tapp {nty} {nvl}.
Arguments vt {nty} {nvl}.
Arguments var_vl {nty} {nvl}.
Arguments lam {nty} {nvl}.
Arguments tlam {nty} {nvl}.
Instance Subst_ty { mty : nat } { nty : nat } : Subst1 (fin (mty) → ty (nty)) (ty (mty)) (ty (nty)) := @subst_ty (mty) (nty) .
Instance Subst_tm { mty mvl : nat } { nty nvl : nat } : Subst2 (fin (mty) → ty (nty)) (fin (mvl) → vl (nty) (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @subst_tm (mty) (mvl) (nty) (nvl) .
Instance Subst_vl { mty mvl : nat } { nty nvl : nat } : Subst2 (fin (mty) → ty (nty)) (fin (mvl) → vl (nty) (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @subst_vl (mty) (mvl) (nty) (nvl) .
Instance Ren_ty { mty : nat } { nty : nat } : Ren1 (fin (mty) → fin (nty)) (ty (mty)) (ty (nty)) := @ren_ty (mty) (nty) .
Instance Ren_tm { mty mvl : nat } { nty nvl : nat } : Ren2 (fin (mty) → fin (nty)) (fin (mvl) → fin (nvl)) (tm (mty) (mvl)) (tm (nty) (nvl)) := @ren_tm (mty) (mvl) (nty) (nvl) .
Instance Ren_vl { mty mvl : nat } { nty nvl : nat } : Ren2 (fin (mty) → fin (nty)) (fin (mvl) → fin (nvl)) (vl (mty) (mvl)) (vl (nty) (nvl)) := @ren_vl (mty) (mvl) (nty) (nvl) .
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_vl { mty mvl : nat } : Var (fin (mvl)) (vl (mty) (mvl)) := @var_vl (mty) (mvl) .
Notation "x '__vl'" := (var_vl x) (at level 5, format "x __vl") : subst_scope.
Notation "x '__vl'" := (@ids (_) (_) VarInstance_vl x) (at level 5, only printing, format "x __vl") : subst_scope.
Notation "'var'" := (var_vl) (only printing, at level 1) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_ty) (only printing) : subst_scope.
Notation "⇑__ty" := (up_ty_vl) (only printing) : subst_scope.
Notation "⇑__vl" := (up_vl_ty) (only printing) : subst_scope.
Notation "⇑__vl" := (up_vl_vl) (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 ; sigmavl ]" := (subst_tm sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "s ⟨ xity ; xivl ⟩" := (ren_tm xity xivl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmaty ; sigmavl ]" := (subst_tm sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.
Notation "⟨ xity ; xivl ⟩" := (ren_tm xity xivl) (at level 1, left associativity, only printing) : fscope.
Notation "s [ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "s ⟨ xity ; xivl ⟩" := (ren_vl xity xivl s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmaty ; sigmavl ]" := (subst_vl sigmaty sigmavl) (at level 1, left associativity, only printing) : fscope.
Notation "⟨ xity ; xivl ⟩" := (ren_vl xity xivl) (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, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, ren1, subst2, ren2, Subst1, Ren1, Subst2, Ren2, ids, Subst_ty, Subst_tm, Subst_vl, Ren_ty, Ren_tm, Ren_vl, VarInstance_ty, VarInstance_vl in ×.
Ltac asimpl' := repeat first [progress rewrite ?instId_ty| progress rewrite ?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 ?instId_vl| progress rewrite ?rinstId_vl| progress rewrite ?compComp_vl| progress rewrite ?compComp'_vl| progress rewrite ?compRen_vl| progress rewrite ?compRen'_vl| progress rewrite ?renComp_vl| progress rewrite ?renComp'_vl| progress rewrite ?renRen_vl| progress rewrite ?renRen'_vl| progress rewrite ?varL_ty| progress rewrite ?varLRen_ty| progress rewrite ?varL_vl| progress rewrite ?varLRen_vl| progress (unfold up_ren, upRen_ty_ty, upRen_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, up_ty_ty, up_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_ty in *| progress rewrite ?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 ?instId_vl in *| progress rewrite ?rinstId_vl in *| progress rewrite ?compComp_vl in *| progress rewrite ?compComp'_vl in *| progress rewrite ?compRen_vl in *| progress rewrite ?compRen'_vl in *| progress rewrite ?renComp_vl in *| progress rewrite ?renComp'_vl in *| progress rewrite ?renRen_vl in *| progress rewrite ?renRen'_vl in *| progress rewrite ?varL_ty in *| progress rewrite ?varLRen_ty in *| progress rewrite ?varL_vl in *| progress rewrite ?varLRen_vl in *| progress (unfold up_ren, upRen_ty_ty, upRen_ty_ty, upRen_ty_vl, upRen_vl_ty, upRen_vl_vl, up_ty_ty, up_ty_ty, up_ty_vl, up_vl_ty, up_vl_vl in *)| progress (cbn [subst_ty subst_tm subst_vl ren_ty ren_tm ren_vl] in *)| fsimpl in *].
Ltac substify := auto_unfold; try repeat (erewrite rinst_inst_ty; [|now intros]); try repeat (erewrite rinst_inst_tm; [|now intros]); try repeat (erewrite rinst_inst_vl; [|now intros]).
Ltac renamify := auto_unfold; try repeat (erewrite <- rinst_inst_ty; [|intros; now asimpl]); try repeat (erewrite <- rinst_inst_tm; [|intros; now asimpl]); try repeat (erewrite <- rinst_inst_vl; [|intros; now asimpl]).