Require Export fintype. Require Export header_extensible.
Section tm.
Inductive tm (ntm : nat) : Type :=
| var_tm : (fin) (ntm) -> tm (ntm)
| atom : tm (ntm)
| plus : tm (ntm) -> tm (ntm) -> tm (ntm).
Lemma congr_atom { mtm : nat } : atom (mtm) = atom (mtm) .
Proof. congruence. Qed.
Lemma congr_plus { mtm : nat } { s0 : tm (mtm) } { s1 : tm (mtm) } { t0 : tm (mtm) } { t1 : tm (mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : plus (mtm) s0 s1 = plus (mtm) t0 t1 .
Proof. congruence. Qed.
Fixpoint subst_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (s : tm (mtm)) : tm (ntm) :=
match s with
| var_tm (_) s => sigmatm s
| atom (_) => atom (ntm)
| plus (_) s0 s1 => plus (ntm) ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1)
end.
Definition up_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) : (fin) ((S) (m)) -> tm ((S) ntm) :=
(scons) ((var_tm ((S) ntm)) (var_zero)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift))) sigma).
Definition upList_tm_tm (p : nat) { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) : (fin) (p+ (m)) -> tm (p+ ntm) :=
scons_p p ((funcomp) (var_tm (p+ ntm)) (zero_p p)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) sigma).
Definition upId_tm_tm { mtm : nat } (sigma : (fin) (mtm) -> tm (mtm)) (Eq : forall x, sigma x = (var_tm (mtm)) x) : forall x, (up_tm_tm sigma) x = (var_tm ((S) mtm)) x :=
fun n => match n with
| Some fin_n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)
| None => eq_refl
end.
Definition upIdList_tm_tm { p : nat } { mtm : nat } (sigma : (fin) (mtm) -> tm (mtm)) (Eq : forall x, sigma x = (var_tm (mtm)) x) : forall x, (upList_tm_tm p sigma) x = (var_tm (p+ mtm)) x :=
fun n => scons_p_eta (var_tm (p+ mtm)) (fun n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n)) (fun n => eq_refl).
Fixpoint idSubst_tm { mtm : nat } (sigmatm : (fin) (mtm) -> tm (mtm)) (Eqtm : forall x, sigmatm x = (var_tm (mtm)) x) (s : tm (mtm)) : subst_tm sigmatm s = s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1)
end.
Definition upExt_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) (tau : (fin) (m) -> tm (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (up_tm_tm sigma) x = (up_tm_tm tau) x :=
fun n => match n with
| Some fin_n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)
| None => eq_refl
end.
Definition upExt_list_tm_tm { p : nat } { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) (tau : (fin) (m) -> tm (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (upList_tm_tm p sigma) x = (upList_tm_tm p tau) x :=
fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n)).
Fixpoint ext_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (tautm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, sigmatm x = tautm x) (s : tm (mtm)) : subst_tm sigmatm s = subst_tm tautm s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1)
end.
Fixpoint compSubstSubst_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1)
end.
Definition up_subst_subst_tm_tm { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (tautm : (fin) (ltm) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_tm_tm tautm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| Some fin_n => (eq_trans) (compSubstSubst_tm ((funcomp) (var_tm (_)) (shift)) (up_tm_tm tautm) ((funcomp) (up_tm_tm tautm) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstSubst_tm tautm ((funcomp) (var_tm (_)) (shift)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift))) tautm) (fun x => eq_refl) (sigma fin_n))) ((ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)))
| None => eq_refl
end.
Definition up_subst_subst_list_tm_tm { p : nat } { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (tautm : (fin) (ltm) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (upList_tm_tm p tautm)) (upList_tm_tm p sigma)) x = (upList_tm_tm p theta) x :=
fun n => (eq_trans) (scons_p_comp' ((funcomp) (var_tm (p+ ltm)) (zero_p p)) (_) (_) n) (scons_p_congr (fun x => scons_p_head' (_) (fun z => subst_tm ((funcomp) (var_tm (_)) (shift_p p)) (_)) x) (fun n => (eq_trans) (compSubstSubst_tm ((funcomp) (var_tm (_)) (shift_p p)) (upList_tm_tm p tautm) ((funcomp) (upList_tm_tm p tautm) (shift_p p)) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstSubst_tm tautm ((funcomp) (var_tm (_)) (shift_p p)) (_) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (sigma n))) ((ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n))))).
Lemma instId_tm { mtm : nat } : subst_tm (var_tm (mtm)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_tm (var_tm (mtm)) (fun n => eq_refl) ((id) x))). Qed.
Lemma varL_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) : (funcomp) (subst_tm sigmatm) (var_tm (mtm)) = sigmatm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma compComp_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_tm sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_tm tautm) (subst_tm sigmatm) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmatm tautm n)). Qed.
End tm.
Section form.
Inductive form (ntm : nat) : Type :=
| fal : form (ntm)
| pred : tm (ntm) -> form (ntm)
| all : form ((S) ntm) -> form (ntm).
Lemma congr_fal { mtm : nat } : fal (mtm) = fal (mtm) .
Proof. congruence. Qed.
Lemma congr_pred { mtm : nat } { s0 : tm (mtm) } { t0 : tm (mtm) } (H1 : s0 = t0) : pred (mtm) s0 = pred (mtm) t0 .
Proof. congruence. Qed.
Lemma congr_all { mtm : nat } { s0 : form ((S) mtm) } { t0 : form ((S) mtm) } (H1 : s0 = t0) : all (mtm) s0 = all (mtm) t0 .
Proof. congruence. Qed.
Fixpoint subst_form { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (s : form (mtm)) : form (ntm) :=
match s with
| fal (_) => fal (ntm)
| pred (_) s0 => pred (ntm) ((subst_tm sigmatm) s0)
| all (_) s0 => all (ntm) ((subst_form (up_tm_tm sigmatm)) s0)
end.
Fixpoint idSubst_form { mtm : nat } (sigmatm : (fin) (mtm) -> tm (mtm)) (Eqtm : forall x, sigmatm x = (var_tm (mtm)) x) (s : form (mtm)) : subst_form sigmatm s = s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((idSubst_tm sigmatm Eqtm) s0)
| all (_) s0 => congr_all ((idSubst_form (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s0)
end.
Fixpoint ext_form { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (tautm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, sigmatm x = tautm x) (s : form (mtm)) : subst_form sigmatm s = subst_form tautm s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((ext_tm sigmatm tautm Eqtm) s0)
| all (_) s0 => congr_all ((ext_form (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s0)
end.
Fixpoint compSubstSubst_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : form (mtm)) : subst_form tautm (subst_form sigmatm s) = subst_form thetatm s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0)
| all (_) s0 => congr_all ((compSubstSubst_form (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s0)
end.
Lemma instId_form { mtm : nat } : subst_form (var_tm (mtm)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_form (var_tm (mtm)) (fun n => eq_refl) ((id) x))). Qed.
Lemma compComp_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : form (mtm)) : subst_form tautm (subst_form sigmatm s) = subst_form ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_form sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_form tautm) (subst_form sigmatm) = subst_form ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_form sigmatm tautm n)). Qed.
End form.
Arguments var_tm {ntm}.
Arguments atom {ntm}.
Arguments plus {ntm}.
Arguments fal {ntm}.
Arguments pred {ntm}.
Arguments all {ntm}.
Global Instance Subst_tm { mtm : nat } { ntm : nat } : Subst1 ((fin) (mtm) -> tm (ntm)) (tm (mtm)) (tm (ntm)) := @subst_tm (mtm) (ntm) .
Global Instance Subst_form { mtm : nat } { ntm : nat } : Subst1 ((fin) (mtm) -> tm (ntm)) (form (mtm)) (form (ntm)) := @subst_form (mtm) (ntm) .
Global Instance VarInstance_tm { mtm : nat } : Var ((fin) (mtm)) (tm (mtm)) := @var_tm (mtm) .
Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.
Notation "x '__tm'" := (@ids (_) (_) VarInstance_tm x) (at level 5, only printing, format "x __tm") : subst_scope.
Notation "'var'" := (var_tm) (only printing, at level 1) : subst_scope.
Class Up_tm X Y := up_tm : X -> Y.
Notation "↑__tm" := (up_tm) (only printing) : subst_scope.
Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.
Global Instance Up_tm_tm { m : nat } { ntm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (ntm) .
Notation "s [ sigmatm ]" := (subst_tm sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_tm sigmatm) (at level 1, left associativity, only printing) : fscope.
Notation "s [ sigmatm ]" := (subst_form sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_form sigmatm) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Subst_form, VarInstance_tm.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Subst_form, VarInstance_tm in *.
Ltac asimpl' := repeat first [progress rewrite ?instId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_tm| progress rewrite ?instId_form| progress rewrite ?compComp_form| progress rewrite ?compComp'_form| progress rewrite ?varL_tm| progress (unfold up_ren, up_tm_tm, upList_tm_tm)| progress (cbn [subst_tm subst_form])| 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_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_tm in *| progress rewrite ?instId_form in *| progress rewrite ?compComp_form in *| progress rewrite ?compComp'_form in *| progress rewrite ?varL_tm in *| progress (unfold up_ren, up_tm_tm, upList_tm_tm in *)| progress (cbn [subst_tm subst_form] in *)| fsimpl in *].
Ltac substify := auto_unfold.
Ltac renamify := auto_unfold.
Section tm.
Inductive tm (ntm : nat) : Type :=
| var_tm : (fin) (ntm) -> tm (ntm)
| atom : tm (ntm)
| plus : tm (ntm) -> tm (ntm) -> tm (ntm).
Lemma congr_atom { mtm : nat } : atom (mtm) = atom (mtm) .
Proof. congruence. Qed.
Lemma congr_plus { mtm : nat } { s0 : tm (mtm) } { s1 : tm (mtm) } { t0 : tm (mtm) } { t1 : tm (mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : plus (mtm) s0 s1 = plus (mtm) t0 t1 .
Proof. congruence. Qed.
Fixpoint subst_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (s : tm (mtm)) : tm (ntm) :=
match s with
| var_tm (_) s => sigmatm s
| atom (_) => atom (ntm)
| plus (_) s0 s1 => plus (ntm) ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1)
end.
Definition up_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) : (fin) ((S) (m)) -> tm ((S) ntm) :=
(scons) ((var_tm ((S) ntm)) (var_zero)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift))) sigma).
Definition upList_tm_tm (p : nat) { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) : (fin) (p+ (m)) -> tm (p+ ntm) :=
scons_p p ((funcomp) (var_tm (p+ ntm)) (zero_p p)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) sigma).
Definition upId_tm_tm { mtm : nat } (sigma : (fin) (mtm) -> tm (mtm)) (Eq : forall x, sigma x = (var_tm (mtm)) x) : forall x, (up_tm_tm sigma) x = (var_tm ((S) mtm)) x :=
fun n => match n with
| Some fin_n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)
| None => eq_refl
end.
Definition upIdList_tm_tm { p : nat } { mtm : nat } (sigma : (fin) (mtm) -> tm (mtm)) (Eq : forall x, sigma x = (var_tm (mtm)) x) : forall x, (upList_tm_tm p sigma) x = (var_tm (p+ mtm)) x :=
fun n => scons_p_eta (var_tm (p+ mtm)) (fun n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n)) (fun n => eq_refl).
Fixpoint idSubst_tm { mtm : nat } (sigmatm : (fin) (mtm) -> tm (mtm)) (Eqtm : forall x, sigmatm x = (var_tm (mtm)) x) (s : tm (mtm)) : subst_tm sigmatm s = s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1)
end.
Definition upExt_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) (tau : (fin) (m) -> tm (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (up_tm_tm sigma) x = (up_tm_tm tau) x :=
fun n => match n with
| Some fin_n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)
| None => eq_refl
end.
Definition upExt_list_tm_tm { p : nat } { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) (tau : (fin) (m) -> tm (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (upList_tm_tm p sigma) x = (upList_tm_tm p tau) x :=
fun n => scons_p_congr (fun n => eq_refl) (fun n => (ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n)).
Fixpoint ext_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (tautm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, sigmatm x = tautm x) (s : tm (mtm)) : subst_tm sigmatm s = subst_tm tautm s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1)
end.
Fixpoint compSubstSubst_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s with
| var_tm (_) s => Eqtm s
| atom (_) => congr_atom
| plus (_) s0 s1 => congr_plus ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1)
end.
Definition up_subst_subst_tm_tm { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (tautm : (fin) (ltm) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_tm_tm tautm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| Some fin_n => (eq_trans) (compSubstSubst_tm ((funcomp) (var_tm (_)) (shift)) (up_tm_tm tautm) ((funcomp) (up_tm_tm tautm) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstSubst_tm tautm ((funcomp) (var_tm (_)) (shift)) ((funcomp) (subst_tm ((funcomp) (var_tm (_)) (shift))) tautm) (fun x => eq_refl) (sigma fin_n))) ((ap) (subst_tm ((funcomp) (var_tm (_)) (shift))) (Eq fin_n)))
| None => eq_refl
end.
Definition up_subst_subst_list_tm_tm { p : nat } { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (tautm : (fin) (ltm) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (upList_tm_tm p tautm)) (upList_tm_tm p sigma)) x = (upList_tm_tm p theta) x :=
fun n => (eq_trans) (scons_p_comp' ((funcomp) (var_tm (p+ ltm)) (zero_p p)) (_) (_) n) (scons_p_congr (fun x => scons_p_head' (_) (fun z => subst_tm ((funcomp) (var_tm (_)) (shift_p p)) (_)) x) (fun n => (eq_trans) (compSubstSubst_tm ((funcomp) (var_tm (_)) (shift_p p)) (upList_tm_tm p tautm) ((funcomp) (upList_tm_tm p tautm) (shift_p p)) (fun x => eq_refl) (sigma n)) ((eq_trans) ((eq_sym) (compSubstSubst_tm tautm ((funcomp) (var_tm (_)) (shift_p p)) (_) (fun x => (eq_sym) (scons_p_tail' (_) (_) x)) (sigma n))) ((ap) (subst_tm ((funcomp) (var_tm (_)) (shift_p p))) (Eq n))))).
Lemma instId_tm { mtm : nat } : subst_tm (var_tm (mtm)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_tm (var_tm (mtm)) (fun n => eq_refl) ((id) x))). Qed.
Lemma varL_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) : (funcomp) (subst_tm sigmatm) (var_tm (mtm)) = sigmatm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma compComp_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_tm sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_tm tautm) (subst_tm sigmatm) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmatm tautm n)). Qed.
End tm.
Section form.
Inductive form (ntm : nat) : Type :=
| fal : form (ntm)
| pred : tm (ntm) -> form (ntm)
| all : form ((S) ntm) -> form (ntm).
Lemma congr_fal { mtm : nat } : fal (mtm) = fal (mtm) .
Proof. congruence. Qed.
Lemma congr_pred { mtm : nat } { s0 : tm (mtm) } { t0 : tm (mtm) } (H1 : s0 = t0) : pred (mtm) s0 = pred (mtm) t0 .
Proof. congruence. Qed.
Lemma congr_all { mtm : nat } { s0 : form ((S) mtm) } { t0 : form ((S) mtm) } (H1 : s0 = t0) : all (mtm) s0 = all (mtm) t0 .
Proof. congruence. Qed.
Fixpoint subst_form { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (s : form (mtm)) : form (ntm) :=
match s with
| fal (_) => fal (ntm)
| pred (_) s0 => pred (ntm) ((subst_tm sigmatm) s0)
| all (_) s0 => all (ntm) ((subst_form (up_tm_tm sigmatm)) s0)
end.
Fixpoint idSubst_form { mtm : nat } (sigmatm : (fin) (mtm) -> tm (mtm)) (Eqtm : forall x, sigmatm x = (var_tm (mtm)) x) (s : form (mtm)) : subst_form sigmatm s = s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((idSubst_tm sigmatm Eqtm) s0)
| all (_) s0 => congr_all ((idSubst_form (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s0)
end.
Fixpoint ext_form { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (tautm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, sigmatm x = tautm x) (s : form (mtm)) : subst_form sigmatm s = subst_form tautm s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((ext_tm sigmatm tautm Eqtm) s0)
| all (_) s0 => congr_all ((ext_form (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s0)
end.
Fixpoint compSubstSubst_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : form (mtm)) : subst_form tautm (subst_form sigmatm s) = subst_form thetatm s :=
match s with
| fal (_) => congr_fal
| pred (_) s0 => congr_pred ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0)
| all (_) s0 => congr_all ((compSubstSubst_form (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s0)
end.
Lemma instId_form { mtm : nat } : subst_form (var_tm (mtm)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_form (var_tm (mtm)) (fun n => eq_refl) ((id) x))). Qed.
Lemma compComp_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : form (mtm)) : subst_form tautm (subst_form sigmatm s) = subst_form ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_form sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_form { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_form tautm) (subst_form sigmatm) = subst_form ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_form sigmatm tautm n)). Qed.
End form.
Arguments var_tm {ntm}.
Arguments atom {ntm}.
Arguments plus {ntm}.
Arguments fal {ntm}.
Arguments pred {ntm}.
Arguments all {ntm}.
Global Instance Subst_tm { mtm : nat } { ntm : nat } : Subst1 ((fin) (mtm) -> tm (ntm)) (tm (mtm)) (tm (ntm)) := @subst_tm (mtm) (ntm) .
Global Instance Subst_form { mtm : nat } { ntm : nat } : Subst1 ((fin) (mtm) -> tm (ntm)) (form (mtm)) (form (ntm)) := @subst_form (mtm) (ntm) .
Global Instance VarInstance_tm { mtm : nat } : Var ((fin) (mtm)) (tm (mtm)) := @var_tm (mtm) .
Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.
Notation "x '__tm'" := (@ids (_) (_) VarInstance_tm x) (at level 5, only printing, format "x __tm") : subst_scope.
Notation "'var'" := (var_tm) (only printing, at level 1) : subst_scope.
Class Up_tm X Y := up_tm : X -> Y.
Notation "↑__tm" := (up_tm) (only printing) : subst_scope.
Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.
Global Instance Up_tm_tm { m : nat } { ntm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (ntm) .
Notation "s [ sigmatm ]" := (subst_tm sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_tm sigmatm) (at level 1, left associativity, only printing) : fscope.
Notation "s [ sigmatm ]" := (subst_form sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_form sigmatm) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Subst_form, VarInstance_tm.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Subst_form, VarInstance_tm in *.
Ltac asimpl' := repeat first [progress rewrite ?instId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_tm| progress rewrite ?instId_form| progress rewrite ?compComp_form| progress rewrite ?compComp'_form| progress rewrite ?varL_tm| progress (unfold up_ren, up_tm_tm, upList_tm_tm)| progress (cbn [subst_tm subst_form])| 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_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_tm in *| progress rewrite ?instId_form in *| progress rewrite ?compComp_form in *| progress rewrite ?compComp'_form in *| progress rewrite ?varL_tm in *| progress (unfold up_ren, up_tm_tm, upList_tm_tm in *)| progress (cbn [subst_tm subst_form] in *)| fsimpl in *].
Ltac substify := auto_unfold.
Ltac renamify := auto_unfold.