Autosubst.SystemF_cbv
This code was automatically generated by Autosubst 2.0 Beta.
The following inductive types were generated:
ty : Type
tm : Type
vl : Type
The following variable constructors were generated:
var_ty : Type
var_vl : Type
Autosubst 2 uses vectors of substitutions. The types of the generated substiutions are listed below:
subst_of subst_of_ty := index -> ty
subst_of subst_of_tm := (index -> ty, index -> vl)
subst_of subst_of_vl := (index -> ty, index -> vl)
Autosubst 2 furthermore generated the following instantiation operations:
subst_ty : subst_of subst_of_ty -> ty -> ty,
also accessible as s.sigma
subst_tm : subst_of subst_of_tm -> tm -> tm,
also accessible as s.sigma
subst_vl : subst_of subst_of_vl -> vl -> vl,
also accessible as s.sigma
See the generated dot-graph for further details.
Automation has been extended to include the generated definitions. The tactic asimpl simplifies goals containing substiution expressions, autosubst corresponds to now asimpl.
If Autosubst 2 does not behave as expected, we are grateful for a short mail to autosubst@ps.uni-saarland.de.
Thank you!
Note: As work-in-progress, some proofs were added by hand. These are marked accordingly.
Require Export Autosubst2.
Set Implicit Arguments.
Require Import Lists.List.
Import ListNotations.
Set Typeclasses Filtered Unification.
Inductive ty : Type :=
| var_ty : index -> ty
| arr : ty -> ty -> ty
| all : ty -> ty.
Definition congr_arr {s0 s1 t0 t1: ty} (E0: s0 = t0) (E1: s1 = t1) : arr s0 s1 = arr t0 t1 :=
apc (ap arr E0) (E1).
Definition congr_all {s0 t0: ty} (E0: s0 = t0) : all s0 = all t0 :=
ap all E0.
Definition subst_of_ty : list Type :=
[ty: Type].
Definition toVarRen_ty (xi: ren_of subst_of_ty) : _ :=
let xi := xi in xi.
Definition upren_ty_ty (xi: ren_of subst_of_ty) : ren_of subst_of_ty :=
let xi_ty := xi in up_ren xi_ty.
Fixpoint ren_ty (xi: ren_of subst_of_ty) (s: ty) : ty :=
match s with
| var_ty x => var_ty ((toVarRen_ty xi) x)
| arr s0 s1 => arr ((ren_ty xi s0)) ((ren_ty xi s1))
| all s0 => all ((ren_ty (upren_ty_ty xi) s0))
end.
Definition toVar_ty (sigma: subst_of subst_of_ty) : _ :=
let sigma := sigma in sigma.
Definition eq_toVar_ty {sigma tau: subst_of subst_of_ty} (E: eq_of_subst sigma tau) (n: index) : toVar_ty sigma n = toVar_ty tau n.
rename sigma into sigma_ty. rename tau into tau_ty. rename E into E_ty.
exact (E_ty n).
Defined.
Definition compren_ty (sigma: subst_of subst_of_ty) (xi: ren_of subst_of_ty) : subst_of subst_of_ty :=
match sigma with
| sigma_ty => fun x => ren_ty xi (sigma_ty x)
end.
Definition up_ty_ty (sigma: subst_of subst_of_ty) : subst_of subst_of_ty :=
match compren_ty sigma S with
| sigma_ty => scons (var_ty 0) sigma_ty
end.
Fixpoint subst_ty (sigma: subst_of subst_of_ty) (s: ty) : ty :=
match s with
| var_ty x => ((toVar_ty sigma) x)
| arr s0 s1 => arr ((subst_ty sigma s0)) ((subst_ty sigma s1))
| all s0 => all ((subst_ty (up_ty_ty sigma) s0))
end.
Definition comp_ty (sigma tau: subst_of subst_of_ty) : subst_of subst_of_ty :=
match sigma with
| sigma_ty => fun x => subst_ty tau (sigma_ty x)
end.
Definition substMixin_ty : substMixin ty :=
{|subst_of_substType := subst_of_ty;inst_of_substType := subst_ty|}.
Canonical Structure substType_ty : substType :=
Eval hnf in @Pack ty substMixin_ty ty.
Definition upId_ty_ty (sigma_ty: index -> ty) (E_ty: sigma_ty == var_ty) : @eq_of_subst subst_of_ty (up_ty_ty sigma_ty) var_ty :=
fun n => match n return (match up_ty_ty sigma_ty with
| tau_ty => tau_ty n = var_ty n
end) with
| 0 => eq_refl
| S n => ap (ren_ty S) (E_ty n)
end.
Fixpoint id_ty (sigma_ty: index -> ty) (E_ty: sigma_ty == var_ty) (s: ty) : subst_ty sigma_ty s = s :=
match s with
| var_ty n => E_ty n
| arr s0 s1 => apc (ap arr (id_ty _ E_ty s0)) ((id_ty _ E_ty s1))
| all s0 => ap all (match upId_ty_ty _ E_ty with
| E_ty => id_ty _ E_ty s0
end)
end.
Definition toSubst_ty (xi: ren_of subst_of_ty) : subst_of subst_of_ty :=
match xi with
| xi_ty => fun x => var_ty (xi_ty x)
end.
Fixpoint compTrans_ren_ren_ty (xi_ty zeta_ty theta_ty: ren) (E_ty: funcomp (xi_ty) (zeta_ty) == theta_ty) (s: ty)
: ren_ty zeta_ty (ren_ty xi_ty s) = ren_ty theta_ty s :=
match s with
| var_ty n => ap var_ty (E_ty n)
| arr s0 s1 => apc (ap arr (compTrans_ren_ren_ty xi_ty zeta_ty theta_ty E_ty s0)) ((compTrans_ren_ren_ty xi_ty zeta_ty theta_ty E_ty s1))
| all s0 => ap all (compTrans_ren_ren_ty (up_ren xi_ty) (up_ren zeta_ty) (up_ren theta_ty) (up_ren_ren xi_ty zeta_ty theta_ty E_ty) s0)
end.
Definition compE_ren_ren_ty (xi_ty zeta_ty: ren) (s: ty) : ren_ty zeta_ty (ren_ty xi_ty s) = ren_ty (funcomp xi_ty zeta_ty) s :=
compTrans_ren_ren_ty xi_ty zeta_ty (funcomp xi_ty zeta_ty) (fun _ => eq_refl) s.
Definition up_ren_subst_ty_ty (xi_ty: ren) (theta_ty tau_ty: index -> ty) (E_ty: (fun x => theta_ty (xi_ty x)) == tau_ty)
: @eq_of_subst subst_of_ty (comp_ty (toSubst_ty (upren_ty_ty xi_ty)) (up_ty_ty theta_ty)) (up_ty_ty tau_ty) :=
fun n => match n return match comp_ty (toSubst_ty (upren_ty_ty xi_ty)) (up_ty_ty theta_ty), up_ty_ty tau_ty with
| xi_ty, tau_ty => xi_ty n = tau_ty n
end with
| 0 => eq_refl
| S n => ap (ren_ty S) (E_ty n)
end.
Fixpoint compTrans_ren_subst_ty (xi_ty: ren) (tau_ty theta_ty: index -> ty) (E_ty: (fun x => tau_ty (xi_ty x)) == theta_ty) (s: ty)
: subst_ty tau_ty (ren_ty xi_ty s) = subst_ty theta_ty s :=
match s with
| var_ty n => (E_ty n)
| arr s0 s1 => apc (ap arr (compTrans_ren_subst_ty xi_ty _ _ E_ty s0)) ((compTrans_ren_subst_ty xi_ty _ _ E_ty s1))
| all s0 => ap all (match up_ren_subst_ty_ty xi_ty tau_ty theta_ty E_ty with
| E_ty => compTrans_ren_subst_ty (up_ren xi_ty) _ _ E_ty s0
end)
end.
Definition compE_ren_subst_ty (xi_ty: ren) (tau_ty: index -> ty) (s: ty)
: subst_ty tau_ty (ren_ty xi_ty s) = subst_ty (funcomp xi_ty tau_ty) s :=
compTrans_ren_subst_ty xi_ty tau_ty (funcomp xi_ty tau_ty) (fun _ => eq_refl) s.
Definition up_subst_ren_ty_ty (sigma_ty: index -> ty)
(rho_ty: ren)
(tau_ty: index -> ty)
(E_ty: (fun x => ren_ty rho_ty (sigma_ty x)) == tau_ty)
: @eq_of_subst subst_of_ty (compren_ty (up_ty_ty sigma_ty) (upren_ty_ty rho_ty)) (up_ty_ty tau_ty) :=
fun n => match n return match compren_ty (up_ty_ty sigma_ty) (upren_ty_ty rho_ty), up_ty_ty tau_ty with
| sigma_ty, tau_ty => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_ren_ty S (up_ren rho_ty) (sigma_ty n)) (eq_trans (eq_sym (compE_ren_ren_ty rho_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end.
Fixpoint compTrans_subst_ren_ty (sigma_ty: index -> ty)
(zeta_ty: ren)
(theta_ty: index -> ty)
(E_ty: (fun x => ren_ty zeta_ty (sigma_ty x)) == theta_ty)
(s: ty) : ren_ty zeta_ty (subst_ty sigma_ty s) = subst_ty theta_ty s :=
match s with
| var_ty n => (E_ty n)
| arr s0 s1 => apc (ap arr (compTrans_subst_ren_ty _ zeta_ty _ E_ty s0)) ((compTrans_subst_ren_ty _ zeta_ty _ E_ty s1))
| all s0 => ap all (match up_subst_ren_ty_ty sigma_ty zeta_ty theta_ty E_ty with
| E_ty => compTrans_subst_ren_ty _ (up_ren zeta_ty) _ E_ty s0
end)
end.
Definition compE_subst_ren_ty (sigma_ty: index -> ty) (zeta_ty: ren) (s: ty)
: ren_ty zeta_ty (subst_ty sigma_ty s) = subst_ty (fun n => ren_ty (zeta_ty) (sigma_ty n)) s :=
compTrans_subst_ren_ty sigma_ty zeta_ty (fun n => ren_ty (zeta_ty) (sigma_ty n)) (fun _ => eq_refl) s.
Definition up_subst_subst_ty_ty (sigma_ty theta_ty tau_ty: index -> ty) (E_ty: (fun x => subst_ty theta_ty (sigma_ty x)) == tau_ty)
: @eq_of_subst subst_of_ty (comp_ty (up_ty_ty sigma_ty) (up_ty_ty theta_ty)) (up_ty_ty tau_ty) :=
fun n => match n return match comp_ty (up_ty_ty sigma_ty) (up_ty_ty theta_ty), up_ty_ty tau_ty with
| sigma_ty, tau_ty => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_subst_ty S _ (sigma_ty n)) (eq_trans (eq_sym (compE_subst_ren_ty theta_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end.
Fixpoint compTrans_subst_subst_ty (sigma_ty tau_ty theta_ty: index -> ty)
(E_ty: (fun x => subst_ty tau_ty (sigma_ty x)) == theta_ty)
(s: ty) : subst_ty tau_ty (subst_ty sigma_ty s) = subst_ty theta_ty s :=
match s with
| var_ty n => (E_ty n)
| arr s0 s1 => apc (ap arr (compTrans_subst_subst_ty _ _ _ E_ty s0)) ((compTrans_subst_subst_ty _ _ _ E_ty s1))
| all s0 => ap all (match up_subst_subst_ty_ty sigma_ty tau_ty theta_ty E_ty with
| E_ty => compTrans_subst_subst_ty _ _ _ E_ty s0
end)
end.
Definition compE_subst_subst_ty (sigma_ty tau_ty: index -> ty) (s: ty)
: subst_ty tau_ty (subst_ty sigma_ty s) = subst_ty (fun n => subst_ty (tau_ty) (sigma_ty n)) s :=
compTrans_subst_subst_ty sigma_ty tau_ty (fun n => subst_ty (tau_ty) (sigma_ty n)) (fun _ => eq_refl) s.
Definition eq_up_ty_ty {sigma tau: subst_of subst_of_ty} (E: eq_of_subst sigma tau) : eq_of_subst (up_ty_ty sigma) (up_ty_ty tau).
rename sigma into sigma_ty. rename tau into tau_ty. rename E into E_ty.
exact (fun i: index => match i return (var_ty 0 .: sigma_ty >>> ren_ty S) i = (var_ty 0 .: tau_ty >>> ren_ty S) i with 0 => eq_refl
| S j => ap _ (E_ty j) end).
Defined.
Fixpoint subst_eq_ty {sigma tau: subst_of subst_of_ty} (E: eq_of_subst sigma tau) (s: ty) : subst_ty sigma s = subst_ty tau s :=
match s with
| var_ty n => eq_toVar_ty E n
| arr s0 s1 => congr_arr (subst_eq_ty E s0) (subst_eq_ty E s1)
| all s0 => congr_all (subst_eq_ty (eq_up_ty_ty E) s0)
end.
Class AsimplInst_ty (s: ty) (sigma: subst_of subst_of_ty) (t: ty) := asimplInstEqn_ty : (subst_ty sigma) s = t .
Hint Mode AsimplInst_ty + + - : typeclass_instance.
Class AsimplSubst_ty (sigma tau: subst_of subst_of_ty) := asimplSubstEqn_ty : match sigma, tau with
| sigma_ty, tau_ty => (forall x, sigma_ty x = tau_ty x)
end .
Hint Mode AsimplSubst_ty + - : typeclass_instance.
Class AsimplComp_ty (sigma tau theta: subst_of subst_of_ty) := asimplCompEqn_ty : match comp_ty sigma tau, theta with
| sigma_tau_ty, theta_ty => (forall x, sigma_tau_ty x = theta_ty x)
end .
Hint Mode AsimplComp_ty + + - : typeclass_instance.
Instance AsimplToVar_ty (sigma_ty: index -> ty) : AsimplGen (toVar_ty sigma_ty) sigma_ty.
Proof. intros x. reflexivity. Qed.
Instance AsimplAsimplInst_ty (s t: ty)
(sigma sigma': subst_of subst_of_ty)
(E_sigma: AsimplSubst_ty sigma sigma')
(E: AsimplInst_ty s sigma' t) : Asimpl (subst_ty sigma s) t.
Proof. rewrite <- E. apply subst_eq_ty. assumption. Qed.
Instance AsimplInstRefl_ty (s: ty) (sigma: subst_of subst_of_ty) : AsimplInst_ty s sigma (s.[ sigma ]) |100.
Proof. reflexivity. Qed.
Instance AsimplInstVar_ty (x y: index)
(sigma: subst_of subst_of_ty)
(sigma': index -> ty)
(s: ty)
(E: AsimplIndex x y)
(E': AsimplGen (toVar_ty sigma) sigma')
(E'': AsimplVarInst y sigma' s) : AsimplInst_ty (var_ty x) sigma s.
Proof. rewrite E. rewrite <- E''. apply E'. Qed.
(* Proof written by hand. *)
Instance asimplInst_arr (s0 s1 s0' s1': _)
(sigma theta_0 theta_1: subst_of subst_of_ty)
(E_0': AsimplSubst_ty (sigma) theta_0)
(E_1': AsimplSubst_ty (sigma) theta_1)
(E_0: AsimplInst_ty s0 theta_0 s0')
(E_1: AsimplInst_ty s1 theta_1 s1') : AsimplInst_ty (arr s0 s1) sigma (arr s0' s1').
Proof.
unfold AsimplInst_ty.
simpl. f_equal.
- rewrite <- E_0. apply subst_eq_ty. assumption.
- rewrite <- E_1. apply subst_eq_ty. assumption.
Qed.
(* Proof written by hand. *)
Instance asimplInst_all (s0 s0': _)
(sigma theta_0: subst_of subst_of_ty)
(E_0': AsimplSubst_ty ((up_ty_ty sigma)) theta_0)
(E_0: AsimplInst_ty s0 theta_0 s0') : AsimplInst_ty (all s0) sigma (all s0').
Proof.
unfold AsimplInst_ty. simpl.
f_equal.
- rewrite <- E_0. apply subst_eq_ty. assumption.
Qed.
Instance AsimplId_ty (s: ty) : AsimplInst_ty s var_ty s.
Proof. apply id_ty; reflexivity. Qed.
(* Proof written by hand. *)
Instance AsimplInstInst_ty (s t: ty)
(sigma sigma' tau sigma_tau: subst_of subst_of_ty)
(E1: AsimplSubst_ty sigma sigma')
(E2: AsimplComp_ty sigma' tau sigma_tau)
(E3: AsimplInst_ty s sigma_tau t) : AsimplInst_ty (subst_ty sigma s) tau t.
Proof.
rewrite <- E3. apply compTrans_subst_subst_ty.
intros x. rewrite E1. apply E2.
Qed.
(* Proof written by hand. *)
Instance AsimplSubstRefl_ty (sigma: subst_of subst_of_ty) : AsimplSubst_ty sigma sigma | 100.
Proof. intros x. reflexivity. Qed.
(* Proof written by hand. *)
Instance AsimplSubstComp_ty (sigma sigma' tau tau' theta: subst_of subst_of_ty)
(E_sigma: AsimplSubst_ty sigma sigma')
(E_tau: AsimplSubst_ty tau tau')
(E: AsimplComp_ty sigma' tau' theta) : AsimplSubst_ty (comp_ty sigma tau) theta |90.
Proof.
intros x. rewrite <- E. unfold comp_ty.
rewrite E_sigma. apply subst_eq_ty. assumption.
Qed.
Instance AsimplSubstCongr_ty (sigma_ty tau_ty: index -> ty) (E_ty: AsimplGen sigma_ty tau_ty) : AsimplSubst_ty sigma_ty tau_ty |95.
Proof. repeat split; assumption. Qed.
Instance AsimplCompRefl_ty (sigma tau: subst_of subst_of_ty) : AsimplComp_ty sigma tau (comp_ty sigma tau) | 100.
Proof. intros x. reflexivity. Qed.
(* Proof written by hand. *)
Instance AsimplCompIdL_ty (sigma: subst_of subst_of_ty)
(tau: index -> ty)
(E: AsimplGen (toVar_ty sigma) tau) : AsimplComp var_ty (subst_ty sigma) tau.
Proof.
intros x. simpl. apply E.
Qed.
Instance AsimplCompIdR_ty (sigma: index -> ty) : AsimplComp sigma (subst_ty var_ty) sigma.
Proof.
intros x. apply id_ty; reflexivity.
Qed.
(* Proof written by hand. *)
Instance AsimplCompAsso_ty (sigma tau theta tau_theta sigma_tau_theta: subst_of subst_of_ty)
(E: AsimplComp_ty tau theta tau_theta)
(E': AsimplComp_ty sigma tau_theta sigma_tau_theta) : AsimplComp_ty (comp_ty sigma tau) theta sigma_tau_theta.
Proof. intros x. rewrite <- E'. unfold comp_ty. erewrite compTrans_subst_subst_ty. reflexivity.
assumption. Qed.
(* Proof written by hand. *)
Instance AsimplCompCongr_ty (sigma_ty theta_ty: index -> ty)
(tau_ty tau: subst_of subst_of_ty)
(E_ty: AsimplSubst_ty (tau) tau_ty)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty) : AsimplComp_ty sigma_ty tau theta_ty.
Proof.
intros x. rewrite <- E_ty'. simpl. apply subst_eq_ty. assumption.
Qed.
(* Proof written by hand. *)
Instance AsimplCompCongr'_ty (sigma_ty theta_ty: index -> ty)
(tau_ty tau: subst_of subst_of_ty)
(E_ty: AsimplSubst_ty (tau) tau_ty)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty) : AsimplComp (subst_ty sigma_ty) (subst_ty tau) (subst_ty theta_ty).
Proof.
intros s. simpl.
erewrite AsimplInstInst_ty.
- reflexivity.
- intros x. reflexivity.
- intros t. rewrite <- E_ty'. apply subst_eq_ty. assumption.
- reflexivity.
Qed.
Instance AsimplRefl_ty (s: ty) : Asimpl s s | 100.
Proof. reflexivity. Qed.
Instance AsimplGenComp_ty (sigma sigma': index -> ty)
(tau tau': subst_of subst_of_ty)
(theta: index -> ty)
(E: AsimplGen sigma sigma')
(E': AsimplSubst_ty tau tau')
(E'': AsimplComp sigma' (subst_ty tau') theta) : AsimplGen (sigma >>> (subst_ty tau) ) theta.
Proof. intros x. rewrite <- E''. simpl. rewrite E. now apply subst_eq_ty. Qed.
(* Proof written by hand. *)
Lemma up_ren_up (xi : ren) (sigma : index -> ty) (E : (xi >>> var_ty) == sigma) :
(upren_ty_ty xi >>> var_ty) == up_ty_ty sigma.
Proof.
intros [|x].
- reflexivity.
- simpl. unfold compren_ty. rewrite <- E. reflexivity.
Qed.
(* Proof written by hand. *)
Lemma ren_inst_ty (xi : ren) (sigma : index -> ty) (s : ty) (E : (xi >>> var_ty) == sigma) :
ren_ty xi s = s.[sigma].
Proof.
revert xi sigma E. induction s; intros xi sigma E.
- apply E.
- simpl. rewrite (IHs1 _ _ E). rewrite (IHs2 _ _ E). reflexivity.
- simpl. rewrite IHs with (sigma := up_ty_ty sigma).
+ reflexivity.
+ apply up_ren_up. assumption.
Qed.
(* Proof written by hand. *)
Instance AsimplSubstUp_ty_ty (sigma_ty tau_ty: index -> ty)
(E_ty: AsimplGen (var_ty 0 .: sigma_ty >>> (subst_ty ((S >>> var_ty)))) tau_ty) : AsimplSubst_ty (up_ty_ty sigma_ty) tau_ty.
Proof.
unfold up_ty_ty. intros x. rewrite <- E_ty.
simpl. destruct x.
- reflexivity.
- simpl. unfold compren_ty. erewrite ren_inst_ty. reflexivity. reflexivity.
Qed.
Typeclasses Opaque toVar_ty.
Inductive tm : Type :=
| app : tm -> tm -> tm
| tapp : tm -> ty -> tm
| vt : vl -> tm
with vl : Type :=
| var_vl : index -> vl
| lam : ty -> tm -> vl
| tlam : tm -> vl.
Definition congr_app {s0 s1 t0 t1: tm} (E0: s0 = t0) (E1: s1 = t1) : app s0 s1 = app t0 t1 :=
apc (ap app E0) (E1).
Definition congr_tapp {s0: tm} {s1: ty} {t0: tm} {t1: ty} (E0: s0 = t0) (E1: s1 = t1) : tapp s0 s1 = tapp t0 t1 :=
apc (ap tapp E0) (E1).
Definition congr_vt {s0 t0: vl} (E0: s0 = t0) : vt s0 = vt t0 :=
ap vt E0.
Definition congr_lam {s0: ty} {s1: tm} {t0: ty} {t1: tm} (E0: s0 = t0) (E1: s1 = t1) : lam s0 s1 = lam t0 t1 :=
apc (ap lam E0) (E1).
Definition congr_tlam {s0 t0: tm} (E0: s0 = t0) : tlam s0 = tlam t0 :=
ap tlam E0.
Definition subst_of_tm : list Type :=
[ty: Type;vl: Type].
Definition subst_of_vl : list Type :=
[ty: Type;vl: Type].
Definition toVarRen_tm (xi: ren_of subst_of_tm) : _ :=
let (_, _) := xi in xi.
Definition toVarRen_vl (xi: ren_of subst_of_vl) : _ :=
let (_, xi) := xi in xi.
Definition castren_tm_ty (xi: ren_of subst_of_tm) : ren_of subst_of_ty :=
let (xi_ty, _) := xi in xi_ty.
Definition castren_tm_vl (xi: ren_of subst_of_tm) : ren_of subst_of_vl :=
let (xi_ty, xi_vl) := xi in (xi_ty, xi_vl).
Definition castren_vl_ty (xi: ren_of subst_of_vl) : ren_of subst_of_ty :=
let (xi_ty, _) := xi in xi_ty.
Definition castren_vl_tm (xi: ren_of subst_of_vl) : ren_of subst_of_tm :=
let (xi_ty, xi_vl) := xi in (xi_ty, xi_vl).
Definition upren_tm_ty (xi: ren_of subst_of_tm) : ren_of subst_of_tm :=
let (xi_ty, xi_vl) := xi in (up_ren xi_ty, xi_vl).
Definition upren_tm_vl (xi: ren_of subst_of_tm) : ren_of subst_of_tm :=
let (xi_ty, xi_vl) := xi in (xi_ty, up_ren xi_vl).
Definition upren_vl_ty (xi: ren_of subst_of_vl) : ren_of subst_of_vl :=
let (xi_ty, xi_vl) := xi in (up_ren xi_ty, xi_vl).
Definition upren_vl_vl (xi: ren_of subst_of_vl) : ren_of subst_of_vl :=
let (xi_ty, xi_vl) := xi in (xi_ty, up_ren xi_vl).
Fixpoint ren_tm (xi: ren_of subst_of_tm) (s: tm) : tm :=
match s with
| app s0 s1 => app ((ren_tm xi s0)) ((ren_tm xi s1))
| tapp s0 s1 => tapp ((ren_tm xi s0)) ((ren_ty (castren_tm_ty xi) s1))
| vt s0 => vt ((ren_vl (castren_tm_vl xi) s0))
end
with ren_vl (xi: ren_of subst_of_vl) (s: vl) : vl :=
match s with
| var_vl x => var_vl ((toVarRen_vl xi) x)
| lam s0 s1 => lam ((ren_ty (castren_vl_ty xi) s0)) ((ren_tm (upren_vl_vl (castren_vl_tm xi)) s1))
| tlam s0 => tlam ((ren_tm (upren_vl_ty (castren_vl_tm xi)) s0))
end.
Definition toVar_tm (sigma: subst_of subst_of_tm) : _ :=
let (_, _) := sigma in sigma.
Definition toVar_vl (sigma: subst_of subst_of_vl) : _ :=
let (_, sigma) := sigma in sigma.
Definition eq_toVar_vl {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) (n: index) : toVar_vl sigma n = toVar_vl tau n.
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (E_vl n).
Defined.
Definition compren_tm (sigma: subst_of subst_of_tm) (xi: ren_of subst_of_tm) : subst_of subst_of_tm :=
match sigma with
| (sigma_ty, sigma_vl) => (fun x => ren_ty (castren_tm_ty xi) (sigma_ty x), fun x => ren_vl (castren_tm_vl xi) (sigma_vl x))
end.
Definition compren_vl (sigma: subst_of subst_of_vl) (xi: ren_of subst_of_vl) : subst_of subst_of_vl :=
match sigma with
| (sigma_ty, sigma_vl) => (fun x => ren_ty (castren_vl_ty xi) (sigma_ty x), fun x => ren_vl xi (sigma_vl x))
end.
Definition up_tm_ty (sigma: subst_of subst_of_tm) : subst_of subst_of_tm :=
match compren_tm sigma (S, idren) with
| (sigma_ty, sigma_vl) => (scons (var_ty 0) sigma_ty, sigma_vl)
end.
Definition up_tm_vl (sigma: subst_of subst_of_tm) : subst_of subst_of_tm :=
match compren_tm sigma (idren, S) with
| (sigma_ty, sigma_vl) => (sigma_ty, scons (var_vl 0) sigma_vl)
end.
Definition up_vl_ty (sigma: subst_of subst_of_vl) : subst_of subst_of_vl :=
match compren_vl sigma (S, idren) with
| (sigma_ty, sigma_vl) => (scons (var_ty 0) sigma_ty, sigma_vl)
end.
Definition up_vl_vl (sigma: subst_of subst_of_vl) : subst_of subst_of_vl :=
match compren_vl sigma (idren, S) with
| (sigma_ty, sigma_vl) => (sigma_ty, scons (var_vl 0) sigma_vl)
end.
Definition cast_tm_ty (sigma: subst_of subst_of_tm) : subst_of subst_of_ty :=
let (sigma_ty, _) := sigma in sigma_ty.
Definition cast_tm_vl (sigma: subst_of subst_of_tm) : subst_of subst_of_vl :=
let (sigma_ty, sigma_vl) := sigma in (sigma_ty, sigma_vl).
Definition cast_vl_ty (sigma: subst_of subst_of_vl) : subst_of subst_of_ty :=
let (sigma_ty, _) := sigma in sigma_ty.
Definition cast_vl_tm (sigma: subst_of subst_of_vl) : subst_of subst_of_tm :=
let (sigma_ty, sigma_vl) := sigma in (sigma_ty, sigma_vl).
Definition eq_cast_tm_ty {sigma tau: subst_of subst_of_tm} (E: eq_of_subst sigma tau) : eq_of_subst (cast_tm_ty sigma) (cast_tm_ty tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (E_ty).
Defined.
Definition eq_cast_tm_vl {sigma tau: subst_of subst_of_tm} (E: eq_of_subst sigma tau) : eq_of_subst (cast_tm_vl sigma) (cast_tm_vl tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (E_ty) (E_vl)).
Defined.
Definition eq_cast_vl_ty {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) : eq_of_subst (cast_vl_ty sigma) (cast_vl_ty tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (E_ty).
Defined.
Definition eq_cast_vl_tm {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) : eq_of_subst (cast_vl_tm sigma) (cast_vl_tm tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (E_ty) (E_vl)).
Defined.
Fixpoint subst_tm (sigma: subst_of subst_of_tm) (s: tm) : tm :=
match s with
| app s0 s1 => app ((subst_tm sigma s0)) ((subst_tm sigma s1))
| tapp s0 s1 => tapp ((subst_tm sigma s0)) ((subst_ty (cast_tm_ty sigma) s1))
| vt s0 => vt ((subst_vl (cast_tm_vl sigma) s0))
end
with subst_vl (sigma: subst_of subst_of_vl) (s: vl) : vl :=
match s with
| var_vl x => ((toVar_vl sigma) x)
| lam s0 s1 => lam ((subst_ty (cast_vl_ty sigma) s0)) ((subst_tm (up_vl_vl (cast_vl_tm sigma)) s1))
| tlam s0 => tlam ((subst_tm (up_vl_ty (cast_vl_tm sigma)) s0))
end.
Definition comp_tm (sigma tau: subst_of subst_of_tm) : subst_of subst_of_tm :=
match sigma with
| (sigma_ty, sigma_vl) => (fun x => subst_ty (cast_tm_ty tau) (sigma_ty x), fun x => subst_vl (cast_tm_vl tau) (sigma_vl x))
end.
Definition comp_vl (sigma tau: subst_of subst_of_vl) : subst_of subst_of_vl :=
match sigma with
| (sigma_ty, sigma_vl) => (fun x => subst_ty (cast_vl_ty tau) (sigma_ty x), fun x => subst_vl tau (sigma_vl x))
end.
Definition substMixin_tm : substMixin tm :=
{|subst_of_substType := subst_of_tm;inst_of_substType := subst_tm|}.
Definition substMixin_vl : substMixin vl :=
{|subst_of_substType := subst_of_vl;inst_of_substType := subst_vl|}.
Canonical Structure substType_tm : substType :=
Eval hnf in @Pack tm substMixin_tm tm.
Canonical Structure substType_vl : substType :=
Eval hnf in @Pack vl substMixin_vl vl.
Definition upId_tm_ty (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl)
: @eq_of_subst subst_of_tm (up_tm_ty (sigma_ty, sigma_vl)) (var_ty, var_vl) :=
conj (fun n => match n return (match up_tm_ty (sigma_ty, sigma_vl) with
| (tau_ty, tau_vl) => tau_ty n = var_ty n
end) with
| 0 => eq_refl
| S n => ap (ren_ty (castren_tm_ty (S, idren))) (E_ty n)
end) (fun n => ap (ren_vl (castren_tm_vl (S, idren))) (E_vl n)).
Definition upId_tm_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl)
: @eq_of_subst subst_of_tm (up_tm_vl (sigma_ty, sigma_vl)) (var_ty, var_vl) :=
conj (fun n => ap (ren_ty (castren_tm_ty (idren, S))) (E_ty n)) (fun n => match n return (match up_tm_vl (sigma_ty, sigma_vl) with
| (tau_ty, tau_vl) => tau_vl n = var_vl n
end) with
| 0 => eq_refl
| S n => ap (ren_vl (castren_tm_vl (idren, S))) (E_vl n)
end).
Definition upId_vl_ty (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl)
: @eq_of_subst subst_of_vl (up_vl_ty (sigma_ty, sigma_vl)) (var_ty, var_vl) :=
conj (fun n => match n return (match up_vl_ty (sigma_ty, sigma_vl) with
| (tau_ty, tau_vl) => tau_ty n = var_ty n
end) with
| 0 => eq_refl
| S n => ap (ren_ty (castren_vl_ty (S, idren))) (E_ty n)
end) (fun n => ap (ren_vl (S, idren)) (E_vl n)).
Definition upId_vl_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl)
: @eq_of_subst subst_of_vl (up_vl_vl (sigma_ty, sigma_vl)) (var_ty, var_vl) :=
conj (fun n => ap (ren_ty (castren_vl_ty (idren, S))) (E_ty n)) (fun n => match n return (match up_vl_vl (sigma_ty, sigma_vl) with
| (tau_ty, tau_vl) => tau_vl n = var_vl n
end) with
| 0 => eq_refl
| S n => ap (ren_vl (idren, S)) (E_vl n)
end).
Fixpoint id_tm (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl) (s: tm)
: subst_tm (sigma_ty, sigma_vl) s = s :=
match s with
| app s0 s1 => apc (ap app (id_tm _ _ E_ty E_vl s0)) ((id_tm _ _ E_ty E_vl s1))
| tapp s0 s1 => apc (ap tapp (id_tm _ _ E_ty E_vl s0)) ((id_ty _ E_ty s1))
| vt s0 => ap vt (id_vl _ _ E_ty E_vl s0)
end
with id_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) (E_ty: sigma_ty == var_ty) (E_vl: sigma_vl == var_vl) (s: vl)
: subst_vl (sigma_ty, sigma_vl) s = s :=
match s with
| var_vl n => E_vl n
| lam s0 s1 => apc (ap lam (id_ty _ E_ty s0)) ((match upId_tm_vl _ _ E_ty E_vl with
| conj (E_ty) (E_vl) => id_tm _ _ E_ty E_vl s1
end))
| tlam s0 => ap tlam (match upId_tm_ty _ _ E_ty E_vl with
| conj (E_ty) (E_vl) => id_tm _ _ E_ty E_vl s0
end)
end.
Definition toSubst_tm (xi: ren_of subst_of_tm) : subst_of subst_of_tm :=
match xi with
| (xi_ty, xi_vl) => (fun x => var_ty (xi_ty x), fun x => var_vl (xi_vl x))
end.
Definition toSubst_vl (xi: ren_of subst_of_vl) : subst_of subst_of_vl :=
match xi with
| (xi_ty, xi_vl) => (fun x => var_ty (xi_ty x), fun x => var_vl (xi_vl x))
end.
Fixpoint compTrans_ren_ren_tm (xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl: ren)
(E_ty: funcomp (xi_ty) (zeta_ty) == theta_ty)
(E_vl: funcomp (xi_vl) (zeta_vl) == theta_vl)
(s: tm) : ren_tm (zeta_ty, zeta_vl) (ren_tm (xi_ty, xi_vl) s) = ren_tm (theta_ty, theta_vl) s :=
match s with
| app s0 s1 =>
apc (ap app (compTrans_ren_ren_tm xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl s0)) ((compTrans_ren_ren_tm xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl s1))
| tapp s0 s1 =>
apc (ap tapp (compTrans_ren_ren_tm xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl s0)) ((compTrans_ren_ren_ty xi_ty zeta_ty theta_ty E_ty s1))
| vt s0 => ap vt (compTrans_ren_ren_vl xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl s0)
end
with compTrans_ren_ren_vl (xi_ty xi_vl zeta_ty zeta_vl theta_ty theta_vl: ren)
(E_ty: funcomp (xi_ty) (zeta_ty) == theta_ty)
(E_vl: funcomp (xi_vl) (zeta_vl) == theta_vl)
(s: vl) : ren_vl (zeta_ty, zeta_vl) (ren_vl (xi_ty, xi_vl) s) = ren_vl (theta_ty, theta_vl) s :=
match s with
| var_vl n => ap var_vl (E_vl n)
| lam s0 s1 =>
apc (ap lam (compTrans_ren_ren_ty xi_ty zeta_ty theta_ty E_ty s0)) ((compTrans_ren_ren_tm xi_ty (up_ren xi_vl) zeta_ty (up_ren zeta_vl) theta_ty (up_ren theta_vl) E_ty (up_ren_ren xi_vl zeta_vl theta_vl E_vl) s1))
| tlam s0 =>
ap tlam (compTrans_ren_ren_tm (up_ren xi_ty) xi_vl (up_ren zeta_ty) zeta_vl (up_ren theta_ty) theta_vl (up_ren_ren xi_ty zeta_ty theta_ty E_ty) E_vl s0)
end.
Definition compE_ren_ren_tm (xi_ty xi_vl zeta_ty zeta_vl: ren) (s: tm) : ren_tm (zeta_ty, zeta_vl) (ren_tm (xi_ty
, xi_vl) s) = ren_tm ((funcomp xi_ty zeta_ty)
, (funcomp xi_vl zeta_vl)) s :=
compTrans_ren_ren_tm xi_ty xi_vl zeta_ty zeta_vl (funcomp xi_ty zeta_ty) (funcomp xi_vl zeta_vl) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition compE_ren_ren_vl (xi_ty xi_vl zeta_ty zeta_vl: ren) (s: vl) : ren_vl (zeta_ty, zeta_vl) (ren_vl (xi_ty
, xi_vl) s) = ren_vl ((funcomp xi_ty zeta_ty)
, (funcomp xi_vl zeta_vl)) s :=
compTrans_ren_ren_vl xi_ty xi_vl zeta_ty zeta_vl (funcomp xi_ty zeta_ty) (funcomp xi_vl zeta_vl) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition up_ren_subst_tm_ty (xi_ty xi_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => theta_ty (xi_ty x)) == tau_ty)
(E_vl: (fun x => theta_vl (xi_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (comp_tm (toSubst_tm (upren_tm_ty (xi_ty
, xi_vl))) (up_tm_ty (theta_ty
, theta_vl))) (up_tm_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match comp_tm (toSubst_tm (upren_tm_ty (xi_ty, xi_vl))) (up_tm_ty (theta_ty, theta_vl)), up_tm_ty (tau_ty
, tau_vl) with
| (xi_ty, xi_vl), (tau_ty, tau_vl) => xi_ty n = tau_ty n
end with
| 0 => eq_refl
| S n => ap (ren_ty (castren_tm_ty (S, idren))) (E_ty n)
end) (fun n => ap (ren_vl (castren_tm_vl (S, idren))) (E_vl n)).
Definition up_ren_subst_tm_vl (xi_ty xi_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => theta_ty (xi_ty x)) == tau_ty)
(E_vl: (fun x => theta_vl (xi_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (comp_tm (toSubst_tm (upren_tm_vl (xi_ty
, xi_vl))) (up_tm_vl (theta_ty
, theta_vl))) (up_tm_vl (tau_ty
, tau_vl)) :=
conj (fun n => ap (ren_ty (castren_tm_ty (idren, S))) (E_ty n)) (fun n => match n return match comp_tm (toSubst_tm (upren_tm_vl (xi_ty
, xi_vl))) (up_tm_vl (theta_ty
, theta_vl)), up_tm_vl (tau_ty
, tau_vl) with
| (xi_ty, xi_vl), (tau_ty, tau_vl) => xi_vl n = tau_vl n
end with
| 0 => eq_refl
| S n => ap (ren_vl (castren_tm_vl (idren, S))) (E_vl n)
end).
Definition up_ren_subst_vl_ty (xi_ty xi_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => theta_ty (xi_ty x)) == tau_ty)
(E_vl: (fun x => theta_vl (xi_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (comp_vl (toSubst_vl (upren_vl_ty (xi_ty
, xi_vl))) (up_vl_ty (theta_ty
, theta_vl))) (up_vl_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match comp_vl (toSubst_vl (upren_vl_ty (xi_ty, xi_vl))) (up_vl_ty (theta_ty, theta_vl)), up_vl_ty (tau_ty
, tau_vl) with
| (xi_ty, xi_vl), (tau_ty, tau_vl) => xi_ty n = tau_ty n
end with
| 0 => eq_refl
| S n => ap (ren_ty (castren_vl_ty (S, idren))) (E_ty n)
end) (fun n => ap (ren_vl (S, idren)) (E_vl n)).
Definition up_ren_subst_vl_vl (xi_ty xi_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => theta_ty (xi_ty x)) == tau_ty)
(E_vl: (fun x => theta_vl (xi_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (comp_vl (toSubst_vl (upren_vl_vl (xi_ty
, xi_vl))) (up_vl_vl (theta_ty
, theta_vl))) (up_vl_vl (tau_ty
, tau_vl)) :=
conj (fun n => ap (ren_ty (castren_vl_ty (idren, S))) (E_ty n)) (fun n => match n return match comp_vl (toSubst_vl (upren_vl_vl (xi_ty
, xi_vl))) (up_vl_vl (theta_ty
, theta_vl)), up_vl_vl (tau_ty
, tau_vl) with
| (xi_ty, xi_vl), (tau_ty, tau_vl) => xi_vl n = tau_vl n
end with
| 0 => eq_refl
| S n => ap (ren_vl (idren, S)) (E_vl n)
end).
Fixpoint compTrans_ren_subst_tm (xi_ty xi_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => tau_ty (xi_ty x)) == theta_ty)
(E_vl: (fun x => tau_vl (xi_vl x)) == theta_vl)
(s: tm) : subst_tm (tau_ty, tau_vl) (ren_tm (xi_ty, xi_vl) s) = subst_tm (theta_ty, theta_vl) s :=
match s with
| app s0 s1 =>
apc (ap app (compTrans_ren_subst_tm xi_ty xi_vl _ _ _ _ E_ty E_vl s0)) ((compTrans_ren_subst_tm xi_ty xi_vl _ _ _ _ E_ty E_vl s1))
| tapp s0 s1 => apc (ap tapp (compTrans_ren_subst_tm xi_ty xi_vl _ _ _ _ E_ty E_vl s0)) ((compTrans_ren_subst_ty xi_ty _ _ E_ty s1))
| vt s0 => ap vt (compTrans_ren_subst_vl xi_ty xi_vl _ _ _ _ E_ty E_vl s0)
end
with compTrans_ren_subst_vl (xi_ty xi_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => tau_ty (xi_ty x)) == theta_ty)
(E_vl: (fun x => tau_vl (xi_vl x)) == theta_vl)
(s: vl) : subst_vl (tau_ty, tau_vl) (ren_vl (xi_ty, xi_vl) s) = subst_vl (theta_ty, theta_vl) s :=
match s with
| var_vl n => (E_vl n)
| lam s0 s1 =>
apc (ap lam (compTrans_ren_subst_ty xi_ty _ _ E_ty s0)) ((match up_ren_subst_vl_vl xi_ty xi_vl tau_ty tau_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_ren_subst_tm xi_ty (up_ren xi_vl) _ _ _ _ E_ty E_vl s1
end))
| tlam s0 => ap tlam (match up_ren_subst_vl_ty xi_ty xi_vl tau_ty tau_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_ren_subst_tm (up_ren xi_ty) xi_vl _ _ _ _ E_ty E_vl s0
end)
end.
Definition compE_ren_subst_tm (xi_ty xi_vl: ren) (tau_ty: index -> ty) (tau_vl: index -> vl) (s: tm) : subst_tm (tau_ty
, tau_vl) (ren_tm (xi_ty
, xi_vl) s) = subst_tm ((funcomp xi_ty tau_ty)
, (funcomp xi_vl tau_vl)) s :=
compTrans_ren_subst_tm xi_ty xi_vl tau_ty tau_vl (funcomp xi_ty tau_ty) (funcomp xi_vl tau_vl) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition compE_ren_subst_vl (xi_ty xi_vl: ren) (tau_ty: index -> ty) (tau_vl: index -> vl) (s: vl) : subst_vl (tau_ty
, tau_vl) (ren_vl (xi_ty
, xi_vl) s) = subst_vl ((funcomp xi_ty tau_ty)
, (funcomp xi_vl tau_vl)) s :=
compTrans_ren_subst_vl xi_ty xi_vl tau_ty tau_vl (funcomp xi_ty tau_ty) (funcomp xi_vl tau_vl) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition up_subst_ren_tm_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(rho_ty rho_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => ren_ty rho_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => ren_vl (rho_ty, rho_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (compren_tm (up_tm_ty (sigma_ty
, sigma_vl)) (upren_tm_ty (rho_ty
, rho_vl))) (up_tm_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match compren_tm (up_tm_ty (sigma_ty, sigma_vl)) (upren_tm_ty (rho_ty, rho_vl)), up_tm_ty (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_ren_ty S (up_ren rho_ty) (sigma_ty n)) (eq_trans (eq_sym (compE_ren_ren_ty rho_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end) (fun n => eq_trans (compE_ren_ren_vl S idren (up_ren rho_ty) rho_vl (sigma_vl n)) (eq_trans (eq_sym (compE_ren_ren_vl rho_ty rho_vl S idren (sigma_vl n))) (ap (ren_vl (S
, idren)) (E_vl n)))).
Definition up_subst_ren_tm_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(rho_ty rho_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => ren_ty rho_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => ren_vl (rho_ty, rho_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (compren_tm (up_tm_vl (sigma_ty
, sigma_vl)) (upren_tm_vl (rho_ty
, rho_vl))) (up_tm_vl (tau_ty
, tau_vl)) :=
conj (fun n => eq_trans (compE_ren_ren_ty idren rho_ty (sigma_ty n)) (eq_trans (eq_sym (compE_ren_ren_ty rho_ty idren (sigma_ty n))) (ap (ren_ty idren) (E_ty n)))) (fun n => match n return match compren_tm (up_tm_vl (sigma_ty
, sigma_vl)) (upren_tm_vl (rho_ty
, rho_vl)), up_tm_vl (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_vl n = tau_vl n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_ren_vl idren S rho_ty (up_ren rho_vl) (sigma_vl n)) (eq_trans (eq_sym (compE_ren_ren_vl rho_ty rho_vl idren S (sigma_vl n))) (ap (ren_vl (idren
, S)) (E_vl n)))
end).
Definition up_subst_ren_vl_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(rho_ty rho_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => ren_ty rho_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => ren_vl (rho_ty, rho_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (compren_vl (up_vl_ty (sigma_ty
, sigma_vl)) (upren_vl_ty (rho_ty
, rho_vl))) (up_vl_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match compren_vl (up_vl_ty (sigma_ty, sigma_vl)) (upren_vl_ty (rho_ty, rho_vl)), up_vl_ty (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_ren_ty S (up_ren rho_ty) (sigma_ty n)) (eq_trans (eq_sym (compE_ren_ren_ty rho_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end) (fun n => eq_trans (compE_ren_ren_vl S idren (up_ren rho_ty) rho_vl (sigma_vl n)) (eq_trans (eq_sym (compE_ren_ren_vl rho_ty rho_vl S idren (sigma_vl n))) (ap (ren_vl (S
, idren)) (E_vl n)))).
Definition up_subst_ren_vl_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(rho_ty rho_vl: ren)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => ren_ty rho_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => ren_vl (rho_ty, rho_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (compren_vl (up_vl_vl (sigma_ty
, sigma_vl)) (upren_vl_vl (rho_ty
, rho_vl))) (up_vl_vl (tau_ty
, tau_vl)) :=
conj (fun n => eq_trans (compE_ren_ren_ty idren rho_ty (sigma_ty n)) (eq_trans (eq_sym (compE_ren_ren_ty rho_ty idren (sigma_ty n))) (ap (ren_ty idren) (E_ty n)))) (fun n => match n return match compren_vl (up_vl_vl (sigma_ty
, sigma_vl)) (upren_vl_vl (rho_ty
, rho_vl)), up_vl_vl (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_vl n = tau_vl n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_ren_vl idren S rho_ty (up_ren rho_vl) (sigma_vl n)) (eq_trans (eq_sym (compE_ren_ren_vl rho_ty rho_vl idren S (sigma_vl n))) (ap (ren_vl (idren
, S)) (E_vl n)))
end).
Fixpoint compTrans_subst_ren_tm (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(zeta_ty zeta_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => ren_ty zeta_ty (sigma_ty x)) == theta_ty)
(E_vl: (fun x => ren_vl (zeta_ty, zeta_vl) (sigma_vl x)) == theta_vl)
(s: tm) : ren_tm (zeta_ty, zeta_vl) (subst_tm (sigma_ty, sigma_vl) s) = subst_tm (theta_ty, theta_vl) s :=
match s with
| app s0 s1 =>
apc (ap app (compTrans_subst_ren_tm _ _ zeta_ty zeta_vl _ _ E_ty E_vl s0)) ((compTrans_subst_ren_tm _ _ zeta_ty zeta_vl _ _ E_ty E_vl s1))
| tapp s0 s1 => apc (ap tapp (compTrans_subst_ren_tm _ _ zeta_ty zeta_vl _ _ E_ty E_vl s0)) ((compTrans_subst_ren_ty _ zeta_ty _ E_ty s1))
| vt s0 => ap vt (compTrans_subst_ren_vl _ _ zeta_ty zeta_vl _ _ E_ty E_vl s0)
end
with compTrans_subst_ren_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(zeta_ty zeta_vl: ren)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => ren_ty zeta_ty (sigma_ty x)) == theta_ty)
(E_vl: (fun x => ren_vl (zeta_ty, zeta_vl) (sigma_vl x)) == theta_vl)
(s: vl) : ren_vl (zeta_ty, zeta_vl) (subst_vl (sigma_ty, sigma_vl) s) = subst_vl (theta_ty, theta_vl) s :=
match s with
| var_vl n => (E_vl n)
| lam s0 s1 =>
apc (ap lam (compTrans_subst_ren_ty _ zeta_ty _ E_ty s0)) ((match up_subst_ren_vl_vl sigma_ty sigma_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_subst_ren_tm _ _ zeta_ty (up_ren zeta_vl) _ _ E_ty E_vl s1
end))
| tlam s0 => ap tlam (match up_subst_ren_vl_ty sigma_ty sigma_vl zeta_ty zeta_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_subst_ren_tm _ _ (up_ren zeta_ty) zeta_vl _ _ E_ty E_vl s0
end)
end.
Definition compE_subst_ren_tm (sigma_ty: index -> ty) (sigma_vl: index -> vl) (zeta_ty zeta_vl: ren) (s: tm) : ren_tm (zeta_ty
, zeta_vl) (subst_tm (sigma_ty
, sigma_vl) s) = subst_tm ((fun n => ren_ty (zeta_ty) (sigma_ty n))
, (fun n => ren_vl ((zeta_ty
, zeta_vl)) (sigma_vl n))) s :=
compTrans_subst_ren_tm sigma_ty sigma_vl zeta_ty zeta_vl (fun n => ren_ty (zeta_ty) (sigma_ty n)) (fun n => ren_vl ((zeta_ty
, zeta_vl)) (sigma_vl n)) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition compE_subst_ren_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) (zeta_ty zeta_vl: ren) (s: vl) : ren_vl (zeta_ty
, zeta_vl) (subst_vl (sigma_ty
, sigma_vl) s) = subst_vl ((fun n => ren_ty (zeta_ty) (sigma_ty n))
, (fun n => ren_vl ((zeta_ty
, zeta_vl)) (sigma_vl n))) s :=
compTrans_subst_ren_vl sigma_ty sigma_vl zeta_ty zeta_vl (fun n => ren_ty (zeta_ty) (sigma_ty n)) (fun n => ren_vl ((zeta_ty
, zeta_vl)) (sigma_vl n)) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition up_subst_subst_tm_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => subst_ty theta_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => subst_vl (theta_ty, theta_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (comp_tm (up_tm_ty (sigma_ty
, sigma_vl)) (up_tm_ty (theta_ty
, theta_vl))) (up_tm_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match comp_tm (up_tm_ty (sigma_ty, sigma_vl)) (up_tm_ty (theta_ty, theta_vl)), up_tm_ty (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_subst_ty S _ (sigma_ty n)) (eq_trans (eq_sym (compE_subst_ren_ty theta_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end) (fun n => eq_trans (compE_ren_subst_vl S idren _ _ (sigma_vl n)) (eq_trans (eq_sym (compE_subst_ren_vl theta_ty theta_vl S idren (sigma_vl n))) (ap (ren_vl (S
, idren)) (E_vl n)))).
Definition up_subst_subst_tm_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => subst_ty theta_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => subst_vl (theta_ty, theta_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_tm (comp_tm (up_tm_vl (sigma_ty
, sigma_vl)) (up_tm_vl (theta_ty
, theta_vl))) (up_tm_vl (tau_ty
, tau_vl)) :=
conj (fun n => eq_trans (compE_ren_subst_ty idren _ (sigma_ty n)) (eq_trans (eq_sym (compE_subst_ren_ty theta_ty idren (sigma_ty n))) (ap (ren_ty idren) (E_ty n)))) (fun n => match n return match comp_tm (up_tm_vl (sigma_ty
, sigma_vl)) (up_tm_vl (theta_ty
, theta_vl)), up_tm_vl (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_vl n = tau_vl n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_subst_vl idren S _ _ (sigma_vl n)) (eq_trans (eq_sym (compE_subst_ren_vl theta_ty theta_vl idren S (sigma_vl n))) (ap (ren_vl (idren
, S)) (E_vl n)))
end).
Definition up_subst_subst_vl_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => subst_ty theta_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => subst_vl (theta_ty, theta_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (comp_vl (up_vl_ty (sigma_ty
, sigma_vl)) (up_vl_ty (theta_ty
, theta_vl))) (up_vl_ty (tau_ty
, tau_vl)) :=
conj (fun n => match n return match comp_vl (up_vl_ty (sigma_ty, sigma_vl)) (up_vl_ty (theta_ty, theta_vl)), up_vl_ty (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_ty n = tau_ty n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_subst_ty S _ (sigma_ty n)) (eq_trans (eq_sym (compE_subst_ren_ty theta_ty S (sigma_ty n))) (ap (ren_ty S) (E_ty n)))
end) (fun n => eq_trans (compE_ren_subst_vl S idren _ _ (sigma_vl n)) (eq_trans (eq_sym (compE_subst_ren_vl theta_ty theta_vl S idren (sigma_vl n))) (ap (ren_vl (S
, idren)) (E_vl n)))).
Definition up_subst_subst_vl_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: (fun x => subst_ty theta_ty (sigma_ty x)) == tau_ty)
(E_vl: (fun x => subst_vl (theta_ty, theta_vl) (sigma_vl x)) == tau_vl) : @eq_of_subst subst_of_vl (comp_vl (up_vl_vl (sigma_ty
, sigma_vl)) (up_vl_vl (theta_ty
, theta_vl))) (up_vl_vl (tau_ty
, tau_vl)) :=
conj (fun n => eq_trans (compE_ren_subst_ty idren _ (sigma_ty n)) (eq_trans (eq_sym (compE_subst_ren_ty theta_ty idren (sigma_ty n))) (ap (ren_ty idren) (E_ty n)))) (fun n => match n return match comp_vl (up_vl_vl (sigma_ty
, sigma_vl)) (up_vl_vl (theta_ty
, theta_vl)), up_vl_vl (tau_ty
, tau_vl) with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => sigma_vl n = tau_vl n
end with
| 0 => eq_refl
| S n =>
eq_trans (compE_ren_subst_vl idren S _ _ (sigma_vl n)) (eq_trans (eq_sym (compE_subst_ren_vl theta_ty theta_vl idren S (sigma_vl n))) (ap (ren_vl (idren
, S)) (E_vl n)))
end).
Fixpoint compTrans_subst_subst_tm (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => subst_ty tau_ty (sigma_ty x)) == theta_ty)
(E_vl: (fun x => subst_vl (tau_ty, tau_vl) (sigma_vl x)) == theta_vl)
(s: tm) : subst_tm (tau_ty, tau_vl) (subst_tm (sigma_ty, sigma_vl) s) = subst_tm (theta_ty, theta_vl) s :=
match s with
| app s0 s1 => apc (ap app (compTrans_subst_subst_tm _ _ _ _ _ _ E_ty E_vl s0)) ((compTrans_subst_subst_tm _ _ _ _ _ _ E_ty E_vl s1))
| tapp s0 s1 => apc (ap tapp (compTrans_subst_subst_tm _ _ _ _ _ _ E_ty E_vl s0)) ((compTrans_subst_subst_ty _ _ _ E_ty s1))
| vt s0 => ap vt (compTrans_subst_subst_vl _ _ _ _ _ _ E_ty E_vl s0)
end
with compTrans_subst_subst_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(E_ty: (fun x => subst_ty tau_ty (sigma_ty x)) == theta_ty)
(E_vl: (fun x => subst_vl (tau_ty, tau_vl) (sigma_vl x)) == theta_vl)
(s: vl) : subst_vl (tau_ty, tau_vl) (subst_vl (sigma_ty, sigma_vl) s) = subst_vl (theta_ty, theta_vl) s :=
match s with
| var_vl n => (E_vl n)
| lam s0 s1 =>
apc (ap lam (compTrans_subst_subst_ty _ _ _ E_ty s0)) ((match up_subst_subst_vl_vl sigma_ty sigma_vl tau_ty tau_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_subst_subst_tm _ _ _ _ _ _ E_ty E_vl s1
end))
| tlam s0 => ap tlam (match up_subst_subst_vl_ty sigma_ty sigma_vl tau_ty tau_vl theta_ty theta_vl E_ty E_vl with
| conj (E_ty) (E_vl) => compTrans_subst_subst_tm _ _ _ _ _ _ E_ty E_vl s0
end)
end.
Definition compE_subst_subst_tm (sigma_ty: index -> ty) (sigma_vl: index -> vl) (tau_ty: index -> ty) (tau_vl: index -> vl) (s: tm)
: subst_tm (tau_ty, tau_vl) (subst_tm (sigma_ty, sigma_vl) s) = subst_tm ((fun n => subst_ty (tau_ty) (sigma_ty n))
, (fun n => subst_vl ((tau_ty, tau_vl)) (sigma_vl n))) s :=
compTrans_subst_subst_tm sigma_ty sigma_vl tau_ty tau_vl (fun n => subst_ty (tau_ty) (sigma_ty n)) (fun n => subst_vl ((tau_ty
, tau_vl)) (sigma_vl n)) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition compE_subst_subst_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) (tau_ty: index -> ty) (tau_vl: index -> vl) (s: vl)
: subst_vl (tau_ty, tau_vl) (subst_vl (sigma_ty, sigma_vl) s) = subst_vl ((fun n => subst_ty (tau_ty) (sigma_ty n))
, (fun n => subst_vl ((tau_ty, tau_vl)) (sigma_vl n))) s :=
compTrans_subst_subst_vl sigma_ty sigma_vl tau_ty tau_vl (fun n => subst_ty (tau_ty) (sigma_ty n)) (fun n => subst_vl ((tau_ty
, tau_vl)) (sigma_vl n)) (fun _ => eq_refl) (fun _ => eq_refl) s.
Definition eq_up_tm_ty {sigma tau: subst_of subst_of_tm} (E: eq_of_subst sigma tau) : eq_of_subst (up_tm_ty sigma) (up_tm_ty tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (fun i: index => match i return (var_ty 0 .: sigma_ty >>> ren_ty (castren_tm_ty (S
, idren))) i = (var_ty 0 .: tau_ty >>> ren_ty (castren_tm_ty (S
, idren))) i
with 0 => eq_refl | S j => ap _ (E_ty j) end) (fun i: index => ap _ (E_vl i))).
Defined.
Definition eq_up_tm_vl {sigma tau: subst_of subst_of_tm} (E: eq_of_subst sigma tau) : eq_of_subst (up_tm_vl sigma) (up_tm_vl tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (fun i: index => ap _ (E_ty i)) (fun i: index => match i return (var_vl 0 .: sigma_vl >>> ren_vl (castren_tm_vl (idren
, S))) i = (var_vl 0 .: tau_vl >>> ren_vl (castren_tm_vl (idren
, S))) i
with 0 => eq_refl | S j => ap _ (E_vl j) end)).
Defined.
Definition eq_up_vl_ty {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) : eq_of_subst (up_vl_ty sigma) (up_vl_ty tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (fun i: index => match i return (var_ty 0 .: sigma_ty >>> ren_ty (castren_vl_ty (S
, idren))) i = (var_ty 0 .: tau_ty >>> ren_ty (castren_vl_ty (S
, idren))) i
with 0 => eq_refl | S j => ap _ (E_ty j) end) (fun i: index => ap _ (E_vl i))).
Defined.
Definition eq_up_vl_vl {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) : eq_of_subst (up_vl_vl sigma) (up_vl_vl tau).
destruct sigma as (sigma_ty & sigma_vl). destruct tau as (tau_ty & tau_vl). destruct E as (E_ty & E_vl).
exact (conj (fun i: index => ap _ (E_ty i)) (fun i: index => match i return (var_vl 0 .: sigma_vl >>> ren_vl (idren
, S)) i = (var_vl 0 .: tau_vl >>> ren_vl (idren
, S)) i
with 0 => eq_refl | S j => ap _ (E_vl j) end)).
Defined.
Fixpoint subst_eq_tm {sigma tau: subst_of subst_of_tm} (E: eq_of_subst sigma tau) (s: tm) : subst_tm sigma s = subst_tm tau s :=
match s with
| app s0 s1 => congr_app (subst_eq_tm E s0) (subst_eq_tm E s1)
| tapp s0 s1 => congr_tapp (subst_eq_tm E s0) (subst_eq_ty (eq_cast_tm_ty E) s1)
| vt s0 => congr_vt (subst_eq_vl (eq_cast_tm_vl E) s0)
end
with subst_eq_vl {sigma tau: subst_of subst_of_vl} (E: eq_of_subst sigma tau) (s: vl) : subst_vl sigma s = subst_vl tau s :=
match s with
| var_vl n => eq_toVar_vl E n
| lam s0 s1 => congr_lam (subst_eq_ty (eq_cast_vl_ty E) s0) (subst_eq_tm (eq_up_tm_vl (eq_cast_vl_tm E)) s1)
| tlam s0 => congr_tlam (subst_eq_tm (eq_up_tm_ty (eq_cast_vl_tm E)) s0)
end.
Class AsimplInst_tm (s: tm) (sigma: subst_of subst_of_tm) (t: tm) := asimplInstEqn_tm : (subst_tm sigma) s = t .
Hint Mode AsimplInst_tm + + - : typeclass_instance.
Class AsimplSubst_tm (sigma tau: subst_of subst_of_tm) := asimplSubstEqn_tm : match sigma, tau with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => (forall x, sigma_ty x = tau_ty x) /\ ((forall x, sigma_vl x = tau_vl x))
end .
Hint Mode AsimplSubst_tm + - : typeclass_instance.
Class AsimplComp_tm (sigma tau theta: subst_of subst_of_tm) := asimplCompEqn_tm : match comp_tm sigma tau, theta with
| (sigma_tau_ty, sigma_tau_vl), (theta_ty, theta_vl) => (forall x, sigma_tau_ty x = theta_ty x) /\ ((forall x, sigma_tau_vl x = theta_vl x))
end .
Hint Mode AsimplComp_tm + + - : typeclass_instance.
Class AsimplInst_vl (s: vl) (sigma: subst_of subst_of_vl) (t: vl) := asimplInstEqn_vl : (subst_vl sigma) s = t .
Hint Mode AsimplInst_vl + + - : typeclass_instance.
Class AsimplSubst_vl (sigma tau: subst_of subst_of_vl) := asimplSubstEqn_vl : match sigma, tau with
| (sigma_ty, sigma_vl), (tau_ty, tau_vl) => (forall x, sigma_ty x = tau_ty x) /\ ((forall x, sigma_vl x = tau_vl x))
end .
Hint Mode AsimplSubst_vl + - : typeclass_instance.
Class AsimplComp_vl (sigma tau theta: subst_of subst_of_vl) := asimplCompEqn_vl : match comp_vl sigma tau, theta with
| (sigma_tau_ty, sigma_tau_vl), (theta_ty, theta_vl) => (forall x, sigma_tau_ty x = theta_ty x) /\ ((forall x, sigma_tau_vl x = theta_vl x))
end .
Hint Mode AsimplComp_vl + + - : typeclass_instance.
Instance AsimplCast_tm_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau: subst_of subst_of_ty)
(E: AsimplSubst_ty sigma_ty tau) : AsimplSubst_ty ((cast_tm_ty (sigma_ty, sigma_vl))) tau.
Proof. apply E. Qed.
Typeclasses Opaque cast_tm_ty.
Instance AsimplCast_tm_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau: subst_of subst_of_vl)
(E: AsimplSubst_vl (sigma_ty, sigma_vl) tau) : AsimplSubst_vl ((cast_tm_vl (sigma_ty, sigma_vl))) tau.
Proof. apply E. Qed.
Typeclasses Opaque cast_tm_vl.
Instance AsimplAsimplInst_tm (s t: tm)
(sigma sigma': subst_of subst_of_tm)
(E_sigma: AsimplSubst_tm sigma sigma')
(E: AsimplInst_tm s sigma' t) : Asimpl (subst_tm sigma s) t.
Proof. rewrite <- E. apply subst_eq_tm. assumption. Qed.
Instance AsimplInstRefl_tm (s: tm) (sigma: subst_of subst_of_tm) : AsimplInst_tm s sigma (s.[ sigma ]) |100.
Proof. reflexivity. Qed.
(* Proof written by hand *)
Instance asimplInst_app (s0 s1 s0' s1': _)
(sigma theta_0 theta_1: subst_of subst_of_tm)
(E_0': AsimplSubst_tm (sigma) theta_0)
(E_1': AsimplSubst_tm (sigma) theta_1)
(E_0: AsimplInst_tm s0 theta_0 s0')
(E_1: AsimplInst_tm s1 theta_1 s1') : AsimplInst_tm (app s0 s1) sigma (app s0' s1').
Proof.
unfold AsimplInst_tm. simpl. f_equal.
- rewrite <- E_0. apply subst_eq_tm. assumption.
- rewrite <- E_1. apply subst_eq_tm. assumption.
Qed.
(* Proof written by hand *)
Instance asimplInst_tapp (s0 s1 s0' s1': _)
(sigma theta_0: subst_of subst_of_tm)
(theta_1: subst_of subst_of_ty)
(E_0': AsimplSubst_tm (sigma) theta_0)
(E_1': AsimplSubst_ty (((cast_tm_ty sigma))) theta_1)
(E_0: AsimplInst_tm s0 theta_0 s0')
(E_1: AsimplInst_ty s1 theta_1 s1') : AsimplInst_tm (tapp s0 s1) sigma (tapp s0' s1').
Proof.
unfold AsimplInst_tm. simpl. f_equal.
- rewrite <- E_0. apply subst_eq_tm. assumption.
- rewrite <- E_1. apply subst_eq_ty. assumption.
Qed.
(* Proof written by hand *)
Instance asimplInst_vt (s0 s0': _)
(sigma: subst_of subst_of_tm)
(theta_0: subst_of subst_of_vl)
(E_0': AsimplSubst_vl (((cast_tm_vl sigma))) theta_0)
(E_0: AsimplInst_vl s0 theta_0 s0') : AsimplInst_tm (vt s0) sigma (vt s0').
Proof.
unfold AsimplInst_tm. simpl. f_equal.
- rewrite <- E_0. apply subst_eq_vl. assumption.
Qed.
Instance AsimplId_tm (s: tm) : AsimplInst_tm s (var_ty, var_vl) s.
Proof. apply id_tm; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplInstInst_tm (s t: tm)
(sigma sigma' tau sigma_tau: subst_of subst_of_tm)
(E1: AsimplSubst_tm sigma sigma')
(E2: AsimplComp_tm sigma' tau sigma_tau)
(E3: AsimplInst_tm s sigma_tau t) : AsimplInst_tm (subst_tm sigma s) tau t.
Proof.
rewrite <- E3. destruct sigma, sigma_tau, tau, sigma'.
destruct E1 as [E1_ty E1_vl]. destruct E2 as [E2_ty E2_vl].
apply compTrans_subst_subst_tm.
- intros x. rewrite E1_ty. apply E2_ty.
- intros x. rewrite E1_vl. apply E2_vl.
Qed.
Instance AsimplSubstRefl_tm (sigma: subst_of subst_of_tm) : AsimplSubst_tm sigma sigma | 100.
Proof. destruct sigma; repeat split; intros x; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplSubstComp_tm (sigma sigma' tau tau' theta: subst_of subst_of_tm)
(E_sigma: AsimplSubst_tm sigma sigma')
(E_tau: AsimplSubst_tm tau tau')
(E: AsimplComp_tm sigma' tau' theta) : AsimplSubst_tm (comp_tm sigma tau) theta |90.
Proof.
destruct sigma', tau', tau, theta, sigma.
destruct E as [E_ty E_vl]. destruct E_sigma as [E'_ty E'_vl]. destruct E_tau as [E''_ty E''_vl].
repeat split.
- intros x. simpl. rewrite <- E_ty. rewrite E'_ty. apply subst_eq_ty. assumption.
- intros x. simpl. rewrite <- E_vl. rewrite E'_vl. apply subst_eq_vl. split; assumption.
Qed.
Instance AsimplSubstCongr_tm (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen sigma_ty tau_ty)
(E_vl: AsimplGen sigma_vl tau_vl) : AsimplSubst_tm (sigma_ty, sigma_vl) (tau_ty, tau_vl) |95.
Proof. repeat split; assumption. Qed.
Instance AsimplCompRefl_tm (sigma tau: subst_of subst_of_tm) : AsimplComp_tm sigma tau (comp_tm sigma tau) | 100.
Proof. destruct sigma; destruct tau; repeat split; intros x; reflexivity. Qed.
Instance AsimplCompIdR_tm (sigma: index -> tm) : AsimplComp sigma (subst_tm (var_ty, var_vl)) sigma.
Proof. intros x. apply id_tm; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplCompAsso_tm (sigma tau theta tau_theta sigma_tau_theta: subst_of subst_of_tm)
(E: AsimplComp_tm tau theta tau_theta)
(E': AsimplComp_tm sigma tau_theta sigma_tau_theta) : AsimplComp_tm (comp_tm sigma tau) theta sigma_tau_theta.
Proof.
destruct tau, theta, tau_theta, sigma, sigma_tau_theta.
destruct E as [E_ty E_vl]. destruct E' as [E'_ty E'_vl].
unfold AsimplComp_tm. simpl. split; intros x.
- rewrite <- E'_ty. simpl. erewrite compTrans_subst_subst_ty.
+ reflexivity.
+ assumption.
- rewrite <- E'_vl. simpl. erewrite compTrans_subst_subst_vl.
+ reflexivity.
+ assumption.
+ assumption.
Qed.
(* Proof written by hand *)
Instance AsimplCompCongr_tm (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: subst_of subst_of_ty)
(tau_vl: subst_of subst_of_vl)
(tau: subst_of subst_of_tm)
(E_ty: AsimplSubst_ty ((cast_tm_ty tau)) tau_ty)
(E_vl: AsimplSubst_vl ((cast_tm_vl tau)) tau_vl)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty)
(E_vl': AsimplComp sigma_vl (subst_vl tau_vl) theta_vl) : AsimplComp_tm (sigma_ty, sigma_vl) tau (theta_ty, theta_vl).
Proof.
unfold AsimplComp_tm. split.
- intros x. rewrite <- E_ty'. simpl. apply subst_eq_ty. assumption.
- intros x. rewrite <- E_vl'. simpl. apply subst_eq_vl. assumption.
Qed.
(* Proof written by hand *)
Instance AsimplCompCongr'_tm (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: subst_of subst_of_ty)
(tau_vl: subst_of subst_of_vl)
(tau: subst_of subst_of_tm)
(E_ty: AsimplSubst_ty ((cast_tm_ty tau)) tau_ty)
(E_vl: AsimplSubst_vl ((cast_tm_vl tau)) tau_vl)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty)
(E_vl': AsimplComp sigma_vl (subst_vl tau_vl) theta_vl) : AsimplComp (subst_tm (sigma_ty, sigma_vl)) (subst_tm tau) (subst_tm (theta_ty
, theta_vl)).
Proof.
intros s. simpl. erewrite AsimplInstInst_tm.
- reflexivity.
- instantiate (1 := (sigma_ty, sigma_vl)). split; reflexivity.
- instantiate (1 := (theta_ty, theta_vl)).
unfold AsimplComp_tm. simpl. split.
+ intros x. rewrite <- E_ty'. simpl. apply subst_eq_ty. assumption.
+ intros x. rewrite <- E_vl'. simpl. apply subst_eq_vl. assumption.
- reflexivity.
Qed.
Instance AsimplRefl_tm (s: tm) : Asimpl s s | 100.
Proof. reflexivity. Qed.
Instance AsimplGenComp_tm (sigma sigma': index -> tm)
(tau tau': subst_of subst_of_tm)
(theta: index -> tm)
(E: AsimplGen sigma sigma')
(E': AsimplSubst_tm tau tau')
(E'': AsimplComp sigma' (subst_tm tau') theta) : AsimplGen (sigma >>> (subst_tm tau) ) theta.
Proof. intros x. rewrite <- E''. simpl. rewrite E. now apply subst_eq_tm. Qed.
(* Lemma up_ren_up (xi : ren) (sigma : index -> ty) (E : (xi >>> var_ty) == sigma) :
(upren_ty_ty xi >>> var_ty) == up_ty_ty sigma.
Proof.
intros |x.
- reflexivity.
- simpl. unfold compren_ty. rewrite <- E. reflexivity.
Qed. *)
(* Proof written by hand. *)
Definition up_ren_up_vl_vl (xi zeta : ren) (sigma : index -> ty) (tau: index -> vl) (E_ty : (xi >>> var_ty) == sigma) (E_vl: (zeta >>> var_vl) == tau) :
@eq_of_subst subst_of_tm (xi >>> var_ty, up_ren zeta >>> var_vl) (up_vl_vl (sigma, tau)).
Proof.
split.
- intros x. simpl. rewrite <- E_ty.
reflexivity.
- intros x. simpl. destruct x.
+ reflexivity.
+ simpl. rewrite <- E_vl. reflexivity.
Qed.
Definition up_ren_up_vl_ty (xi zeta : ren) (sigma : index -> ty) (tau: index -> vl) (E_ty : (xi >>> var_ty) == sigma) (E_vl: (zeta >>> var_vl) == tau) :
@eq_of_subst subst_of_tm (up_ren xi >>> var_ty, zeta >>> var_vl) (up_vl_ty (sigma, tau)).
Proof.
split.
- intros x. simpl. destruct x; [reflexivity|].
simpl. rewrite <- E_ty. reflexivity.
- intros x. simpl. rewrite <- E_vl. simpl. reflexivity.
Qed.
Print subst_tm.
(* Proof written by hand. *)
Fixpoint ren_inst_tm (xi zeta : ren) (sigma : index -> ty) (tau: index -> vl) (E_ty : (xi >>> var_ty) == sigma) (E_vl: (zeta >>> var_vl) == tau) (s : tm):
ren_tm (xi, zeta) s = s.[(sigma, tau)]
with ren_inst_vl (xi zeta : ren) (sigma : index -> ty) (tau: index -> vl) (E_ty : (xi >>> var_ty) == sigma) (E_vl: (zeta >>> var_vl) == tau) (s : vl):
ren_vl (xi, zeta) s = s.[(sigma, tau)].
Proof.
- induction s.
+ simpl. rewrite IHs1. rewrite IHs2. reflexivity.
+ simpl. rewrite IHs.
erewrite ren_inst_ty. reflexivity. assumption.
+ simpl. erewrite ren_inst_vl.
reflexivity. assumption. assumption.
- induction s.
+ simpl. apply E_vl.
+ simpl. erewrite ren_inst_ty; try eassumption.
destruct (@up_ren_up_vl_vl xi zeta sigma tau E_ty E_vl) as (H1&H2).
rewrite ren_inst_tm with (sigma := fun x : index => ren_ty idren (sigma x)) (tau := var_vl 0 .: (fun x : index => ren_vl (idren, S) (tau x))).
* reflexivity.
* apply H1.
* apply H2.
+ simpl.
destruct (@up_ren_up_vl_ty xi zeta sigma tau E_ty E_vl) as (H1&H2).
rewrite ren_inst_tm with (sigma := var_ty 0 .: (fun x : index => ren_ty S (sigma x))) (tau := fun x : index => ren_vl (S, idren) (tau x)).
* reflexivity.
* apply H1.
* apply H2.
Qed.
(* Proof written by hand *)
Instance AsimplSubstUp_tm_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen (var_ty 0 .: sigma_ty >>> (subst_ty ((cast_tm_ty ((S >>> var_ty, id >>> var_vl)))))) tau_ty)
(E_vl: AsimplGen ( sigma_vl >>> (subst_vl ((cast_tm_vl ((S >>> var_ty, id >>> var_vl)))))) tau_vl) : AsimplSubst_tm (up_tm_ty (sigma_ty
, sigma_vl)) (tau_ty
, tau_vl).
Proof.
split.
- intros x. rewrite <- E_ty. destruct x; [reflexivity|].
simpl. erewrite ren_inst_ty; reflexivity.
- intros x. rewrite <- E_vl.
simpl. erewrite ren_inst_vl; reflexivity.
Qed.
(* Proof written by hand *)
Instance AsimplSubstUp_tm_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen ( sigma_ty >>> (subst_ty ((cast_tm_ty ((id >>> var_ty, S >>> var_vl)))))) tau_ty)
(E_vl: AsimplGen (var_vl 0 .: sigma_vl >>> (subst_vl ((cast_tm_vl ((id >>> var_ty
, S >>> var_vl)))))) tau_vl) : AsimplSubst_tm (up_tm_vl (sigma_ty
, sigma_vl)) (tau_ty
, tau_vl).
Proof.
split.
- intros x. rewrite <- E_ty. erewrite ren_inst_ty; reflexivity.
- intros x. rewrite <- E_vl. destruct x; [reflexivity|].
simpl. erewrite ren_inst_vl; reflexivity.
Qed.
Instance AsimplCast_vl_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau: subst_of subst_of_ty)
(E: AsimplSubst_ty sigma_ty tau) : AsimplSubst_ty ((cast_vl_ty (sigma_ty, sigma_vl))) tau.
Proof. apply E. Qed.
Typeclasses Opaque cast_vl_ty.
Instance AsimplToVar_vl (sigma_ty: index -> ty) (sigma_vl: index -> vl) : AsimplGen (toVar_vl (sigma_ty, sigma_vl)) sigma_vl.
Proof. intros x. reflexivity. Qed.
Instance AsimplAsimplInst_vl (s t: vl)
(sigma sigma': subst_of subst_of_vl)
(E_sigma: AsimplSubst_vl sigma sigma')
(E: AsimplInst_vl s sigma' t) : Asimpl (subst_vl sigma s) t.
Proof. rewrite <- E. apply subst_eq_vl. assumption. Qed.
Instance AsimplInstRefl_vl (s: vl) (sigma: subst_of subst_of_vl) : AsimplInst_vl s sigma (s.[ sigma ]) |100.
Proof. reflexivity. Qed.
Instance AsimplInstVar_vl (x y: index)
(sigma: subst_of subst_of_vl)
(sigma': index -> vl)
(s: vl)
(E: AsimplIndex x y)
(E': AsimplGen (toVar_vl sigma) sigma')
(E'': AsimplVarInst y sigma' s) : AsimplInst_vl (var_vl x) sigma s.
Proof. rewrite E. rewrite <- E''. apply E'. Qed.
(* Proof written by hand *)
Instance asimplInst_lam (s0 s1 s0' s1': _)
(sigma: subst_of subst_of_vl)
(theta_0: subst_of subst_of_ty)
(theta_1: subst_of subst_of_tm)
(E_0': AsimplSubst_ty (((cast_vl_ty sigma))) theta_0)
(E_1': AsimplSubst_tm ((up_vl_vl ((cast_vl_tm sigma)))) theta_1)
(E_0: AsimplInst_ty s0 theta_0 s0')
(E_1: AsimplInst_tm s1 theta_1 s1') : AsimplInst_vl (lam s0 s1) sigma (lam s0' s1').
Proof.
unfold AsimplInst_vl. simpl. f_equal.
- rewrite <- E_0. apply subst_eq_ty. assumption.
- rewrite <- E_1. apply subst_eq_tm. assumption.
Qed.
(* Proof written by hand *)
Instance asimplInst_tlam (s0 s0': _)
(sigma: subst_of subst_of_vl)
(theta_0: subst_of subst_of_tm)
(E_0': AsimplSubst_tm ((up_vl_ty ((cast_vl_tm sigma)))) theta_0)
(E_0: AsimplInst_tm s0 theta_0 s0') : AsimplInst_vl (tlam s0) sigma (tlam s0').
Proof.
unfold AsimplInst_vl. simpl. f_equal.
- rewrite <- E_0. apply subst_eq_tm. assumption.
Qed.
Instance AsimplId_vl (s: vl) : AsimplInst_vl s (var_ty, var_vl) s.
Proof. apply id_vl; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplInstInst_vl (s t: vl)
(sigma sigma' tau sigma_tau: subst_of subst_of_vl)
(E1: AsimplSubst_vl sigma sigma')
(E2: AsimplComp_vl sigma' tau sigma_tau)
(E3: AsimplInst_vl s sigma_tau t) : AsimplInst_vl (subst_vl sigma s) tau t.
Proof.
rewrite <- E3. destruct sigma, sigma_tau, tau, sigma'.
destruct E1 as [E1_ty E1_vl]. destruct E2 as [E2_ty E2_vl].
apply compTrans_subst_subst_vl.
- intros x. rewrite E1_ty. apply E2_ty.
- intros x. rewrite E1_vl. apply E2_vl.
Qed.
Instance AsimplSubstRefl_vl (sigma: subst_of subst_of_vl) : AsimplSubst_vl sigma sigma | 100.
Proof. destruct sigma; repeat split; intros x; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplSubstComp_vl (sigma sigma' tau tau' theta: subst_of subst_of_vl)
(E_sigma: AsimplSubst_vl sigma sigma')
(E_tau: AsimplSubst_vl tau tau')
(E: AsimplComp_vl sigma' tau' theta) : AsimplSubst_vl (comp_vl sigma tau) theta |90.
Proof.
destruct sigma', tau', tau, theta, sigma.
destruct E as [E_ty E_vl]. destruct E_sigma as [E'_ty E'_vl]. destruct E_tau as [E''_ty E''_vl].
repeat split.
- intros x. simpl. rewrite <- E_ty. rewrite E'_ty. apply subst_eq_ty. assumption.
- intros x. simpl. rewrite <- E_vl. rewrite E'_vl. apply subst_eq_vl. split; assumption.
Qed.
Instance AsimplSubstCongr_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen sigma_ty tau_ty)
(E_vl: AsimplGen sigma_vl tau_vl) : AsimplSubst_vl (sigma_ty, sigma_vl) (tau_ty, tau_vl) |95.
Proof. repeat split; assumption. Qed.
Instance AsimplCompRefl_vl (sigma tau: subst_of subst_of_vl) : AsimplComp_vl sigma tau (comp_vl sigma tau) | 100.
Proof. destruct sigma; destruct tau; repeat split; intros x; reflexivity. Qed.
Instance AsimplCompIdL_vl (sigma: subst_of subst_of_vl)
(tau: index -> vl)
(E: AsimplGen (toVar_vl sigma) tau) : AsimplComp var_vl (subst_vl sigma) tau.
Proof.
intros x. rewrite <- E. reflexivity.
Qed.
(* Proof written by hand *)
Instance AsimplCompIdR_vl (sigma: index -> vl) : AsimplComp sigma (subst_vl (var_ty, var_vl)) sigma.
Proof. intros x. apply id_vl; reflexivity. Qed.
(* Proof written by hand *)
Instance AsimplCompAsso_vl (sigma tau theta tau_theta sigma_tau_theta: subst_of subst_of_vl)
(E: AsimplComp_vl tau theta tau_theta)
(E': AsimplComp_vl sigma tau_theta sigma_tau_theta) : AsimplComp_vl (comp_vl sigma tau) theta sigma_tau_theta.
Proof.
destruct tau, theta, tau_theta, sigma, sigma_tau_theta.
destruct E as [E_ty E_vl]. destruct E' as [E'_ty E'_vl].
unfold AsimplComp_tm. simpl. split; intros x.
- rewrite <- E'_ty. simpl. erewrite compTrans_subst_subst_ty.
+ reflexivity.
+ assumption.
- rewrite <- E'_vl. simpl. erewrite compTrans_subst_subst_vl.
+ reflexivity.
+ assumption.
+ assumption.
Qed.
(* Proof written by hand *)
Instance AsimplCompCongr_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: subst_of subst_of_ty)
(tau_vl tau: subst_of subst_of_vl)
(E_ty: AsimplSubst_ty ((cast_vl_ty tau)) tau_ty)
(E_vl: AsimplSubst_vl (tau) tau_vl)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty)
(E_vl': AsimplComp sigma_vl (subst_vl tau_vl) theta_vl) : AsimplComp_vl (sigma_ty, sigma_vl) tau (theta_ty, theta_vl).
Proof.
unfold AsimplComp_tm. split.
- intros x. rewrite <- E_ty'. simpl. apply subst_eq_ty. assumption.
- intros x. rewrite <- E_vl'. simpl. apply subst_eq_vl. assumption.
Qed.
(* Proof written by hand *)
Instance AsimplCompCongr'_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(theta_ty: index -> ty)
(theta_vl: index -> vl)
(tau_ty: subst_of subst_of_ty)
(tau_vl tau: subst_of subst_of_vl)
(E_ty: AsimplSubst_ty ((cast_vl_ty tau)) tau_ty)
(E_vl: AsimplSubst_vl (tau) tau_vl)
(E_ty': AsimplComp sigma_ty (subst_ty tau_ty) theta_ty)
(E_vl': AsimplComp sigma_vl (subst_vl tau_vl) theta_vl) : AsimplComp (subst_vl (sigma_ty, sigma_vl)) (subst_vl tau) (subst_vl (theta_ty
, theta_vl)).
Proof.
intros s. simpl. erewrite AsimplInstInst_vl.
- reflexivity.
- instantiate (1 := (sigma_ty, sigma_vl)). split; reflexivity.
- instantiate (1 := (theta_ty, theta_vl)).
unfold AsimplComp_tm. simpl. split.
+ intros x. rewrite <- E_ty'. simpl. apply subst_eq_ty. assumption.
+ intros x. rewrite <- E_vl'. simpl. apply subst_eq_vl. assumption.
- reflexivity.
Qed.
Instance AsimplRefl_vl (s: vl) : Asimpl s s | 100.
Proof. reflexivity. Qed.
Instance AsimplGenComp_vl (sigma sigma': index -> vl)
(tau tau': subst_of subst_of_vl)
(theta: index -> vl)
(E: AsimplGen sigma sigma')
(E': AsimplSubst_vl tau tau')
(E'': AsimplComp sigma' (subst_vl tau') theta) : AsimplGen (sigma >>> (subst_vl tau) ) theta.
Proof. intros x. rewrite <- E''. simpl. rewrite E. now apply subst_eq_vl. Qed.
(* Proof written by hand *)
Instance AsimplSubstUp_vl_ty (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen (var_ty 0 .: sigma_ty >>> (subst_ty ((cast_vl_ty ((S >>> var_ty, id >>> var_vl)))))) tau_ty)
(E_vl: AsimplGen ( sigma_vl >>> (subst_vl (((S >>> var_ty, id >>> var_vl))))) tau_vl) : AsimplSubst_vl (up_vl_ty (sigma_ty
, sigma_vl)) (tau_ty
, tau_vl).
Proof.
split.
- intros x. rewrite <- E_ty. destruct x; [reflexivity|]. simpl.
erewrite ren_inst_ty; reflexivity.
- intros x. rewrite <- E_vl.
erewrite ren_inst_vl; reflexivity.
Qed.
(* Proof written by hand *)
Instance AsimplSubstUp_vl_vl (sigma_ty: index -> ty)
(sigma_vl: index -> vl)
(tau_ty: index -> ty)
(tau_vl: index -> vl)
(E_ty: AsimplGen ( sigma_ty >>> (subst_ty ((cast_vl_ty ((id >>> var_ty, S >>> var_vl)))))) tau_ty)
(E_vl: AsimplGen (var_vl 0 .: sigma_vl >>> (subst_vl (((id >>> var_ty, S >>> var_vl))))) tau_vl) : AsimplSubst_vl (up_vl_vl (sigma_ty
, sigma_vl)) (tau_ty
, tau_vl).
Proof.
split.
- intros x. rewrite <- E_ty. simpl.
erewrite ren_inst_ty; reflexivity.
- intros x. rewrite <- E_vl. destruct x; [reflexivity|]. simpl.
erewrite ren_inst_vl; reflexivity.
Qed.
Typeclasses Opaque toVar_vl.