From Undecidability.HOU Require Import std.std.
From Undecidability.HOU Require Export unscoped.
Set Default Proof Using "Type".
Section Terms.
Inductive type : Type :=
| typevar : nat -> type
| arr : type -> type -> type .
Structure Const :=
{
const_type:> Type;
const_dis: Dis const_type;
ctype: const_type -> type
}.
Context {X: Const}.
Lemma congr_typevar { s0 : nat } { t0 : nat } : s0 = t0 -> typevar s0 = typevar t0 .
Proof. congruence. Qed.
Lemma congr_arr { s0 : type } { s1 : type } { t0 : type } { t1 : type } : s0 = t0 -> s1 = t1 -> arr s0 s1 = arr t0 t1 .
Proof. congruence. Qed.
Inductive exp : Type :=
| var_exp : fin -> exp
| const : X -> exp
| lam : exp -> exp
| app : exp -> exp -> exp .
Lemma congr_const { s0 : X } { t0 : X } : s0 = t0 -> const s0 = const t0 .
Proof. congruence. Qed.
Lemma congr_lam { s0 : exp } { t0 : exp } : s0 = t0 -> lam s0 = lam t0 .
Proof. congruence. Qed.
Lemma congr_app { s0 : exp } { s1 : exp } { t0 : exp } { t1 : exp } : s0 = t0 -> s1 = t1 -> app s0 s1 = app t0 t1 .
Proof. congruence. Qed.
Definition upRen_exp_exp (xi : fin -> fin ) : _ :=
up_ren xi.
Fixpoint ren_exp (xiexp : fin -> fin ) (s : exp ) : _ :=
match s with
| var_exp s => (var_exp ) (xiexp s)
| const s0 => const s0
| lam s0 => lam (ren_exp (upRen_exp_exp xiexp) s0)
| app s0 s1 => app (ren_exp xiexp s0) (ren_exp xiexp s1)
end.
Definition up_exp_exp (sigma : fin -> exp ) : _ :=
scons ((var_exp ) var_zero) (funcomp (ren_exp shift) sigma).
Fixpoint subst_exp (sigmaexp : fin -> exp ) (s : exp ) : _ :=
match s with
| var_exp s => sigmaexp s
| const s0 => const s0
| lam s0 => lam (subst_exp (up_exp_exp sigmaexp) s0)
| app s0 s1 => app (subst_exp sigmaexp s0) (subst_exp sigmaexp s1)
end.
Definition upId_exp_exp (sigma : fin -> exp ) (Eq : forall x, sigma x = (var_exp ) x) : forall x, (up_exp_exp sigma) x = (var_exp ) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint idSubst_exp (sigmaexp : fin -> exp ) (Eqexp : forall x, sigmaexp x = (var_exp ) x) (s : exp ) : subst_exp sigmaexp s = s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (idSubst_exp (up_exp_exp sigmaexp) (upId_exp_exp (_) Eqexp) s0)
| app s0 s1 => congr_app (idSubst_exp sigmaexp Eqexp s0) (idSubst_exp sigmaexp Eqexp s1)
end.
Definition upExtRen_exp_exp (xi : fin -> fin ) (zeta : fin -> fin ) (Eq : forall x, xi x = zeta x) : forall x, (upRen_exp_exp xi) x = (upRen_exp_exp zeta) x :=
fun n => match n with
| S n => ap shift (Eq n)
| 0 => eq_refl
end.
Fixpoint extRen_exp (xiexp : fin -> fin ) (zetaexp : fin -> fin ) (Eqexp : forall x, xiexp x = zetaexp x) (s : exp ) : ren_exp xiexp s = ren_exp zetaexp s :=
match s with
| var_exp s => ap (var_exp ) (Eqexp s)
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (extRen_exp (upRen_exp_exp xiexp) (upRen_exp_exp zetaexp) (upExtRen_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (extRen_exp xiexp zetaexp Eqexp s0) (extRen_exp xiexp zetaexp Eqexp s1)
end.
Definition upExt_exp_exp (sigma : fin -> exp ) (tau : fin -> exp ) (Eq : forall x, sigma x = tau x) : forall x, (up_exp_exp sigma) x = (up_exp_exp tau) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint ext_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (Eqexp : forall x, sigmaexp x = tauexp x) (s : exp ) : subst_exp sigmaexp s = subst_exp tauexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (ext_exp (up_exp_exp sigmaexp) (up_exp_exp tauexp) (upExt_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (ext_exp sigmaexp tauexp Eqexp s0) (ext_exp sigmaexp tauexp Eqexp s1)
end.
Fixpoint compRenRen_exp (xiexp : fin -> fin ) (zetaexp : fin -> fin ) (rhoexp : fin -> fin ) (Eqexp : forall x, (funcomp zetaexp xiexp) x = rhoexp x) (s : exp ) : ren_exp zetaexp (ren_exp xiexp s) = ren_exp rhoexp s :=
match s with
| var_exp s => ap (var_exp ) (Eqexp s)
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compRenRen_exp (upRen_exp_exp xiexp) (upRen_exp_exp zetaexp) (upRen_exp_exp rhoexp) (up_ren_ren (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compRenRen_exp xiexp zetaexp rhoexp Eqexp s0) (compRenRen_exp xiexp zetaexp rhoexp Eqexp s1)
end.
Definition up_ren_subst_exp_exp (xi : fin -> fin ) (tau : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (up_exp_exp tau) (upRen_exp_exp xi)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint compRenSubst_exp (xiexp : fin -> fin ) (tauexp : fin -> exp ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp tauexp xiexp) x = thetaexp x) (s : exp ) : subst_exp tauexp (ren_exp xiexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compRenSubst_exp (upRen_exp_exp xiexp) (up_exp_exp tauexp) (up_exp_exp thetaexp) (up_ren_subst_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compRenSubst_exp xiexp tauexp thetaexp Eqexp s0) (compRenSubst_exp xiexp tauexp thetaexp Eqexp s1)
end.
Definition up_subst_ren_exp_exp (sigma : fin -> exp ) (zetaexp : fin -> fin ) (theta : fin -> exp ) (Eq : forall x, (funcomp (ren_exp zetaexp) sigma) x = theta x) : forall x, (funcomp (ren_exp (upRen_exp_exp zetaexp)) (up_exp_exp sigma)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => eq_trans (compRenRen_exp shift (upRen_exp_exp zetaexp) (funcomp shift zetaexp) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_exp zetaexp shift (funcomp shift zetaexp) (fun x => eq_refl) (sigma n))) (ap (ren_exp shift) (Eq n)))
| 0 => eq_refl
end.
Fixpoint compSubstRen__exp (sigmaexp : fin -> exp ) (zetaexp : fin -> fin ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp (ren_exp zetaexp) sigmaexp) x = thetaexp x) (s : exp ) : ren_exp zetaexp (subst_exp sigmaexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compSubstRen__exp (up_exp_exp sigmaexp) (upRen_exp_exp zetaexp) (up_exp_exp thetaexp) (up_subst_ren_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s0) (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s1)
end.
Definition up_subst_subst_exp_exp (sigma : fin -> exp ) (tauexp : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp (subst_exp tauexp) sigma) x = theta x) : forall x, (funcomp (subst_exp (up_exp_exp tauexp)) (up_exp_exp sigma)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => eq_trans (compRenSubst_exp shift (up_exp_exp tauexp) (funcomp (up_exp_exp tauexp) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__exp tauexp shift (funcomp (ren_exp shift) tauexp) (fun x => eq_refl) (sigma n))) (ap (ren_exp shift) (Eq n)))
| 0 => eq_refl
end.
Fixpoint compSubstSubst_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp (subst_exp tauexp) sigmaexp) x = thetaexp x) (s : exp ) : subst_exp tauexp (subst_exp sigmaexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compSubstSubst_exp (up_exp_exp sigmaexp) (up_exp_exp tauexp) (up_exp_exp thetaexp) (up_subst_subst_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compSubstSubst_exp sigmaexp tauexp thetaexp Eqexp s0) (compSubstSubst_exp sigmaexp tauexp thetaexp Eqexp s1)
end.
Definition rinstInst_up_exp_exp (xi : fin -> fin ) (sigma : fin -> exp ) (Eq : forall x, (funcomp (var_exp ) xi) x = sigma x) : forall x, (funcomp (var_exp ) (upRen_exp_exp xi)) x = (up_exp_exp sigma) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint rinst_inst_exp (xiexp : fin -> fin ) (sigmaexp : fin -> exp ) (Eqexp : forall x, (funcomp (var_exp ) xiexp) x = sigmaexp x) (s : exp ) : ren_exp xiexp s = subst_exp sigmaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (rinst_inst_exp (upRen_exp_exp xiexp) (up_exp_exp sigmaexp) (rinstInst_up_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (rinst_inst_exp xiexp sigmaexp Eqexp s0) (rinst_inst_exp xiexp sigmaexp Eqexp s1)
end.
Lemma instId_exp : subst_exp (var_exp ) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => idSubst_exp (var_exp ) (fun n => eq_refl) (id x))). Qed.
Lemma varL_exp (sigmaexp : fin -> exp ) : funcomp (subst_exp sigmaexp) (var_exp ) = sigmaexp .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => eq_refl)). Qed.
Lemma rinstInst_exp (xiexp : fin -> fin ) : ren_exp xiexp = subst_exp (funcomp (var_exp ) xiexp) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => rinst_inst_exp xiexp (_) (fun n => eq_refl) x)). Qed.
Lemma compComp_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (s : exp ) : subst_exp tauexp (subst_exp sigmaexp s) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) s .
Proof. exact (compSubstSubst_exp sigmaexp tauexp (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) : funcomp (subst_exp tauexp) (subst_exp sigmaexp) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => compComp_exp sigmaexp tauexp n)). Qed.
End Terms.
Definition beta {X} (s: exp) (t: exp) := @subst_exp X (t .: var_exp) s.
Hint Rewrite @instId_exp @rinstInst_exp @compComp_exp @compComp'_exp @varL_exp : asimpl.
Hint Unfold beta upRen_exp_exp up_exp_exp : asimpl.
Ltac asimpl := autounfold with asimpl; autorewrite with asimpl using (cbn [subst_exp ren_exp]; fsimpl).
Tactic Notation "asimpl" "in" hyp(J) :=
autounfold with asimpl in J; autorewrite with asimpl in J using (cbn [subst_exp ren_exp] in J; fsimplin J).
From Undecidability.HOU Require Export unscoped.
Set Default Proof Using "Type".
Section Terms.
Inductive type : Type :=
| typevar : nat -> type
| arr : type -> type -> type .
Structure Const :=
{
const_type:> Type;
const_dis: Dis const_type;
ctype: const_type -> type
}.
Context {X: Const}.
Lemma congr_typevar { s0 : nat } { t0 : nat } : s0 = t0 -> typevar s0 = typevar t0 .
Proof. congruence. Qed.
Lemma congr_arr { s0 : type } { s1 : type } { t0 : type } { t1 : type } : s0 = t0 -> s1 = t1 -> arr s0 s1 = arr t0 t1 .
Proof. congruence. Qed.
Inductive exp : Type :=
| var_exp : fin -> exp
| const : X -> exp
| lam : exp -> exp
| app : exp -> exp -> exp .
Lemma congr_const { s0 : X } { t0 : X } : s0 = t0 -> const s0 = const t0 .
Proof. congruence. Qed.
Lemma congr_lam { s0 : exp } { t0 : exp } : s0 = t0 -> lam s0 = lam t0 .
Proof. congruence. Qed.
Lemma congr_app { s0 : exp } { s1 : exp } { t0 : exp } { t1 : exp } : s0 = t0 -> s1 = t1 -> app s0 s1 = app t0 t1 .
Proof. congruence. Qed.
Definition upRen_exp_exp (xi : fin -> fin ) : _ :=
up_ren xi.
Fixpoint ren_exp (xiexp : fin -> fin ) (s : exp ) : _ :=
match s with
| var_exp s => (var_exp ) (xiexp s)
| const s0 => const s0
| lam s0 => lam (ren_exp (upRen_exp_exp xiexp) s0)
| app s0 s1 => app (ren_exp xiexp s0) (ren_exp xiexp s1)
end.
Definition up_exp_exp (sigma : fin -> exp ) : _ :=
scons ((var_exp ) var_zero) (funcomp (ren_exp shift) sigma).
Fixpoint subst_exp (sigmaexp : fin -> exp ) (s : exp ) : _ :=
match s with
| var_exp s => sigmaexp s
| const s0 => const s0
| lam s0 => lam (subst_exp (up_exp_exp sigmaexp) s0)
| app s0 s1 => app (subst_exp sigmaexp s0) (subst_exp sigmaexp s1)
end.
Definition upId_exp_exp (sigma : fin -> exp ) (Eq : forall x, sigma x = (var_exp ) x) : forall x, (up_exp_exp sigma) x = (var_exp ) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint idSubst_exp (sigmaexp : fin -> exp ) (Eqexp : forall x, sigmaexp x = (var_exp ) x) (s : exp ) : subst_exp sigmaexp s = s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (idSubst_exp (up_exp_exp sigmaexp) (upId_exp_exp (_) Eqexp) s0)
| app s0 s1 => congr_app (idSubst_exp sigmaexp Eqexp s0) (idSubst_exp sigmaexp Eqexp s1)
end.
Definition upExtRen_exp_exp (xi : fin -> fin ) (zeta : fin -> fin ) (Eq : forall x, xi x = zeta x) : forall x, (upRen_exp_exp xi) x = (upRen_exp_exp zeta) x :=
fun n => match n with
| S n => ap shift (Eq n)
| 0 => eq_refl
end.
Fixpoint extRen_exp (xiexp : fin -> fin ) (zetaexp : fin -> fin ) (Eqexp : forall x, xiexp x = zetaexp x) (s : exp ) : ren_exp xiexp s = ren_exp zetaexp s :=
match s with
| var_exp s => ap (var_exp ) (Eqexp s)
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (extRen_exp (upRen_exp_exp xiexp) (upRen_exp_exp zetaexp) (upExtRen_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (extRen_exp xiexp zetaexp Eqexp s0) (extRen_exp xiexp zetaexp Eqexp s1)
end.
Definition upExt_exp_exp (sigma : fin -> exp ) (tau : fin -> exp ) (Eq : forall x, sigma x = tau x) : forall x, (up_exp_exp sigma) x = (up_exp_exp tau) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint ext_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (Eqexp : forall x, sigmaexp x = tauexp x) (s : exp ) : subst_exp sigmaexp s = subst_exp tauexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (ext_exp (up_exp_exp sigmaexp) (up_exp_exp tauexp) (upExt_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (ext_exp sigmaexp tauexp Eqexp s0) (ext_exp sigmaexp tauexp Eqexp s1)
end.
Fixpoint compRenRen_exp (xiexp : fin -> fin ) (zetaexp : fin -> fin ) (rhoexp : fin -> fin ) (Eqexp : forall x, (funcomp zetaexp xiexp) x = rhoexp x) (s : exp ) : ren_exp zetaexp (ren_exp xiexp s) = ren_exp rhoexp s :=
match s with
| var_exp s => ap (var_exp ) (Eqexp s)
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compRenRen_exp (upRen_exp_exp xiexp) (upRen_exp_exp zetaexp) (upRen_exp_exp rhoexp) (up_ren_ren (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compRenRen_exp xiexp zetaexp rhoexp Eqexp s0) (compRenRen_exp xiexp zetaexp rhoexp Eqexp s1)
end.
Definition up_ren_subst_exp_exp (xi : fin -> fin ) (tau : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (up_exp_exp tau) (upRen_exp_exp xi)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint compRenSubst_exp (xiexp : fin -> fin ) (tauexp : fin -> exp ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp tauexp xiexp) x = thetaexp x) (s : exp ) : subst_exp tauexp (ren_exp xiexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compRenSubst_exp (upRen_exp_exp xiexp) (up_exp_exp tauexp) (up_exp_exp thetaexp) (up_ren_subst_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compRenSubst_exp xiexp tauexp thetaexp Eqexp s0) (compRenSubst_exp xiexp tauexp thetaexp Eqexp s1)
end.
Definition up_subst_ren_exp_exp (sigma : fin -> exp ) (zetaexp : fin -> fin ) (theta : fin -> exp ) (Eq : forall x, (funcomp (ren_exp zetaexp) sigma) x = theta x) : forall x, (funcomp (ren_exp (upRen_exp_exp zetaexp)) (up_exp_exp sigma)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => eq_trans (compRenRen_exp shift (upRen_exp_exp zetaexp) (funcomp shift zetaexp) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compRenRen_exp zetaexp shift (funcomp shift zetaexp) (fun x => eq_refl) (sigma n))) (ap (ren_exp shift) (Eq n)))
| 0 => eq_refl
end.
Fixpoint compSubstRen__exp (sigmaexp : fin -> exp ) (zetaexp : fin -> fin ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp (ren_exp zetaexp) sigmaexp) x = thetaexp x) (s : exp ) : ren_exp zetaexp (subst_exp sigmaexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compSubstRen__exp (up_exp_exp sigmaexp) (upRen_exp_exp zetaexp) (up_exp_exp thetaexp) (up_subst_ren_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s0) (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s1)
end.
Definition up_subst_subst_exp_exp (sigma : fin -> exp ) (tauexp : fin -> exp ) (theta : fin -> exp ) (Eq : forall x, (funcomp (subst_exp tauexp) sigma) x = theta x) : forall x, (funcomp (subst_exp (up_exp_exp tauexp)) (up_exp_exp sigma)) x = (up_exp_exp theta) x :=
fun n => match n with
| S n => eq_trans (compRenSubst_exp shift (up_exp_exp tauexp) (funcomp (up_exp_exp tauexp) shift) (fun x => eq_refl) (sigma n)) (eq_trans (eq_sym (compSubstRen__exp tauexp shift (funcomp (ren_exp shift) tauexp) (fun x => eq_refl) (sigma n))) (ap (ren_exp shift) (Eq n)))
| 0 => eq_refl
end.
Fixpoint compSubstSubst_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp (subst_exp tauexp) sigmaexp) x = thetaexp x) (s : exp ) : subst_exp tauexp (subst_exp sigmaexp s) = subst_exp thetaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (compSubstSubst_exp (up_exp_exp sigmaexp) (up_exp_exp tauexp) (up_exp_exp thetaexp) (up_subst_subst_exp_exp (_) (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (compSubstSubst_exp sigmaexp tauexp thetaexp Eqexp s0) (compSubstSubst_exp sigmaexp tauexp thetaexp Eqexp s1)
end.
Definition rinstInst_up_exp_exp (xi : fin -> fin ) (sigma : fin -> exp ) (Eq : forall x, (funcomp (var_exp ) xi) x = sigma x) : forall x, (funcomp (var_exp ) (upRen_exp_exp xi)) x = (up_exp_exp sigma) x :=
fun n => match n with
| S n => ap (ren_exp shift) (Eq n)
| 0 => eq_refl
end.
Fixpoint rinst_inst_exp (xiexp : fin -> fin ) (sigmaexp : fin -> exp ) (Eqexp : forall x, (funcomp (var_exp ) xiexp) x = sigmaexp x) (s : exp ) : ren_exp xiexp s = subst_exp sigmaexp s :=
match s with
| var_exp s => Eqexp s
| const s0 => congr_const (eq_refl s0)
| lam s0 => congr_lam (rinst_inst_exp (upRen_exp_exp xiexp) (up_exp_exp sigmaexp) (rinstInst_up_exp_exp (_) (_) Eqexp) s0)
| app s0 s1 => congr_app (rinst_inst_exp xiexp sigmaexp Eqexp s0) (rinst_inst_exp xiexp sigmaexp Eqexp s1)
end.
Lemma instId_exp : subst_exp (var_exp ) = id .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => idSubst_exp (var_exp ) (fun n => eq_refl) (id x))). Qed.
Lemma varL_exp (sigmaexp : fin -> exp ) : funcomp (subst_exp sigmaexp) (var_exp ) = sigmaexp .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => eq_refl)). Qed.
Lemma rinstInst_exp (xiexp : fin -> fin ) : ren_exp xiexp = subst_exp (funcomp (var_exp ) xiexp) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun x => rinst_inst_exp xiexp (_) (fun n => eq_refl) x)). Qed.
Lemma compComp_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (s : exp ) : subst_exp tauexp (subst_exp sigmaexp s) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) s .
Proof. exact (compSubstSubst_exp sigmaexp tauexp (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) : funcomp (subst_exp tauexp) (subst_exp sigmaexp) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) .
Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => compComp_exp sigmaexp tauexp n)). Qed.
End Terms.
Definition beta {X} (s: exp) (t: exp) := @subst_exp X (t .: var_exp) s.
Hint Rewrite @instId_exp @rinstInst_exp @compComp_exp @compComp'_exp @varL_exp : asimpl.
Hint Unfold beta upRen_exp_exp up_exp_exp : asimpl.
Ltac asimpl := autounfold with asimpl; autorewrite with asimpl using (cbn [subst_exp ren_exp]; fsimpl).
Tactic Notation "asimpl" "in" hyp(J) :=
autounfold with asimpl in J; autorewrite with asimpl in J using (cbn [subst_exp ren_exp] in J; fsimplin J).