Require Import core unscoped.

Require Import Setoid Morphisms Relation_Definitions.


Module Core.

Inductive PTag : Type :=
  | PL : PTag
  | PR : PTag.

Lemma congr_PL : PL = PL.
Proof.
exact (eq_refl).
Qed.

Lemma congr_PR : PR = PR.
Proof.
exact (eq_refl).
Qed.

Inductive PTm : Type :=
  | VarPTm : nat -> PTm
  | PAbs : PTm -> PTm
  | PApp : PTm -> PTm -> PTm
  | PPair : PTm -> PTm -> PTm
  | PProj : PTag -> PTm -> PTm
  | PConst : nat -> PTm.

Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0.
Proof.
exact (eq_trans eq_refl (ap (fun x => PAbs x) H0)).
Qed.

Lemma congr_PApp {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0)
  (H1 : s1 = t1) : PApp s0 s1 = PApp t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp x s1) H0))
         (ap (fun x => PApp t0 x) H1)).
Qed.

Lemma congr_PPair {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0)
  (H1 : s1 = t1) : PPair s0 s1 = PPair t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair x s1) H0))
         (ap (fun x => PPair t0 x) H1)).
Qed.

Lemma congr_PProj {s0 : PTag} {s1 : PTm} {t0 : PTag} {t1 : PTm}
  (H0 : s0 = t0) (H1 : s1 = t1) : PProj s0 s1 = PProj t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0))
         (ap (fun x => PProj t0 x) H1)).
Qed.

Lemma congr_PConst {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
  PConst s0 = PConst t0.
Proof.
exact (eq_trans eq_refl (ap (fun x => PConst x) H0)).
Qed.

Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat.
Proof.
exact (up_ren xi).
Defined.

Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
  match s with
  | VarPTm s0 => VarPTm (xi_PTm s0)
  | PAbs s0 => PAbs (ren_PTm (upRen_PTm_PTm xi_PTm) s0)
  | PApp s0 s1 => PApp (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
  | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
  | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1)
  | PConst s0 => PConst s0
  end.

Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm.
Proof.
exact (scons (VarPTm var_zero) (funcomp (ren_PTm shift) sigma)).
Defined.

Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
  match s with
  | VarPTm s0 => sigma_PTm s0
  | PAbs s0 => PAbs (subst_PTm (up_PTm_PTm sigma_PTm) s0)
  | PApp s0 s1 => PApp (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
  | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
  | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1)
  | PConst s0 => PConst s0
  end.

Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) :
  forall x, up_PTm_PTm sigma x = VarPTm x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_PTm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint idSubst_PTm (sigma_PTm : nat -> PTm)
(Eq_PTm : forall x, sigma_PTm x = VarPTm x) (s : PTm) {struct s} :
subst_PTm sigma_PTm s = s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0)
        (idSubst_PTm sigma_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0)
        (idSubst_PTm sigma_PTm Eq_PTm s1)
  | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
  (Eq : forall x, xi x = zeta x) :
  forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x.
Proof.
exact (fun n => match n with
                | S n' => ap shift (Eq n')
                | O => eq_refl
                end).
Qed.

Fixpoint extRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm) {struct s} :
ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
  match s with
  | VarPTm s0 => ap (VarPTm) (Eq_PTm s0)
  | PAbs s0 =>
      congr_PAbs
        (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upExtRen_PTm_PTm _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
        (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
        (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm)
  (Eq : forall x, sigma x = tau x) :
  forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_PTm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint ext_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm) {struct s} :
subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (upExt_PTm_PTm _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
        (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
        (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
  (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) :
  forall x,
  funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x.
Proof.
exact (up_ren_ren xi zeta rho Eq).
Qed.

Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
(rho_PTm : nat -> nat)
(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm) {struct
 s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s :=
  match s with
  | VarPTm s0 => ap (VarPTm) (Eq_PTm s0)
  | PAbs s0 =>
      congr_PAbs
        (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm)
  (theta : nat -> PTm) (Eq : forall x, funcomp tau xi x = theta x) :
  forall x,
  funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_PTm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
(theta_PTm : nat -> PTm)
(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm) {struct
 s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat)
  (theta : nat -> PTm)
  (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) :
  forall x,
  funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x =
  up_PTm_PTm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' =>
           eq_trans
             (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm)
                (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma n'))
             (eq_trans
                (eq_sym
                   (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm)
                      (fun x => eq_refl) (sigma n')))
                (ap (ren_PTm shift) (Eq n')))
       | O => eq_refl
       end).
Qed.

Fixpoint compSubstRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat)
(theta_PTm : nat -> PTm)
(Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x)
(s : PTm) {struct s} :
ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm)
  (theta : nat -> PTm)
  (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) :
  forall x,
  funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x =
  up_PTm_PTm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' =>
           eq_trans
             (compRenSubst_PTm shift (up_PTm_PTm tau_PTm)
                (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl)
                (sigma n'))
             (eq_trans
                (eq_sym
                   (compSubstRen_PTm tau_PTm shift
                      (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl)
                      (sigma n'))) (ap (ren_PTm shift) (Eq n')))
       | O => eq_refl
       end).
Qed.

Fixpoint compSubstSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
(theta_PTm : nat -> PTm)
(Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x)
(s : PTm) {struct s} :
subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) :
  ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s.
Proof.
exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s).
Qed.

Lemma renRen'_PTm_pointwise (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) :
  pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm))
    (ren_PTm (funcomp zeta_PTm xi_PTm)).
Proof.
exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s).
Qed.

Lemma renSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) (s : PTm) :
  subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s.
Proof.
exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s).
Qed.

Lemma renSubst_PTm_pointwise (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) :
  pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm))
    (subst_PTm (funcomp tau_PTm xi_PTm)).
Proof.
exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s).
Qed.

Lemma substRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) (s : PTm)
  :
  ren_PTm zeta_PTm (subst_PTm sigma_PTm s) =
  subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s.
Proof.
exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s).
Qed.

Lemma substRen_PTm_pointwise (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat)
  :
  pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm))
    (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)).
Proof.
exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s).
Qed.

Lemma substSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
  (s : PTm) :
  subst_PTm tau_PTm (subst_PTm sigma_PTm s) =
  subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s.
Proof.
exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s).
Qed.

Lemma substSubst_PTm_pointwise (sigma_PTm : nat -> PTm)
  (tau_PTm : nat -> PTm) :
  pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm))
    (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)).
Proof.
exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s).
Qed.

Lemma rinstInst_up_PTm_PTm (xi : nat -> nat) (sigma : nat -> PTm)
  (Eq : forall x, funcomp (VarPTm) xi x = sigma x) :
  forall x, funcomp (VarPTm) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_PTm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
(Eq_PTm : forall x, funcomp (VarPTm) xi_PTm x = sigma_PTm x) (s : PTm)
{struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s :=
  match s with
  | VarPTm s0 => Eq_PTm s0
  | PAbs s0 =>
      congr_PAbs
        (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
           (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
  | PApp s0 s1 =>
      congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
        (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
  | PPair s0 s1 =>
      congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
        (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
  end.

Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) :
  ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm) xi_PTm) s.
Proof.
exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s).
Qed.

Lemma rinstInst'_PTm_pointwise (xi_PTm : nat -> nat) :
  pointwise_relation _ eq (ren_PTm xi_PTm)
    (subst_PTm (funcomp (VarPTm) xi_PTm)).
Proof.
exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s).
Qed.

Lemma instId'_PTm (s : PTm) : subst_PTm (VarPTm) s = s.
Proof.
exact (idSubst_PTm (VarPTm) (fun n => eq_refl) s).
Qed.

Lemma instId'_PTm_pointwise : pointwise_relation _ eq (subst_PTm (VarPTm)) id.
Proof.
exact (fun s => idSubst_PTm (VarPTm) (fun n => eq_refl) s).
Qed.

Lemma rinstId'_PTm (s : PTm) : ren_PTm id s = s.
Proof.
exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)).
Qed.

Lemma rinstId'_PTm_pointwise : pointwise_relation _ eq (@ren_PTm id) id.
Proof.
exact (fun s =>
       eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)).
Qed.

Lemma varL'_PTm (sigma_PTm : nat -> PTm) (x : nat) :
  subst_PTm sigma_PTm (VarPTm x) = sigma_PTm x.
Proof.
exact (eq_refl).
Qed.

Lemma varL'_PTm_pointwise (sigma_PTm : nat -> PTm) :
  pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm)) sigma_PTm.
Proof.
exact (fun x => eq_refl).
Qed.

Lemma varLRen'_PTm (xi_PTm : nat -> nat) (x : nat) :
  ren_PTm xi_PTm (VarPTm x) = VarPTm (xi_PTm x).
Proof.
exact (eq_refl).
Qed.

Lemma varLRen'_PTm_pointwise (xi_PTm : nat -> nat) :
  pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm))
    (funcomp (VarPTm) xi_PTm).
Proof.
exact (fun x => eq_refl).
Qed.

Inductive TTag : Type :=
  | TPi : TTag
  | TSig : TTag.

Lemma congr_TPi : TPi = TPi.
Proof.
exact (eq_refl).
Qed.

Lemma congr_TSig : TSig = TSig.
Proof.
exact (eq_refl).
Qed.

Inductive Tm : Type :=
  | VarTm : nat -> Tm
  | Abs : Tm -> Tm -> Tm
  | App : Tm -> Tm -> Tm
  | Pair : Tm -> Tm -> Tm
  | Proj : PTag -> Tm -> Tm
  | TBind : TTag -> Tm -> Tm -> Tm
  | Univ : nat -> Tm
  | BVal : bool -> Tm
  | Bool : Tm
  | If : Tm -> Tm -> Tm -> Tm.

Lemma congr_Abs {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
  (H1 : s1 = t1) : Abs s0 s1 = Abs t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Abs x s1) H0))
         (ap (fun x => Abs t0 x) H1)).
Qed.

Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
  (H1 : s1 = t1) : App s0 s1 = App t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => App x s1) H0))
         (ap (fun x => App t0 x) H1)).
Qed.

Lemma congr_Pair {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
  (H1 : s1 = t1) : Pair s0 s1 = Pair t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair x s1) H0))
         (ap (fun x => Pair t0 x) H1)).
Qed.

Lemma congr_Proj {s0 : PTag} {s1 : Tm} {t0 : PTag} {t1 : Tm} (H0 : s0 = t0)
  (H1 : s1 = t1) : Proj s0 s1 = Proj t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj x s1) H0))
         (ap (fun x => Proj t0 x) H1)).
Qed.

Lemma congr_TBind {s0 : TTag} {s1 : Tm} {s2 : Tm} {t0 : TTag} {t1 : Tm}
  {t2 : Tm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) :
  TBind s0 s1 s2 = TBind t0 t1 t2.
Proof.
exact (eq_trans
         (eq_trans (eq_trans eq_refl (ap (fun x => TBind x s1 s2) H0))
            (ap (fun x => TBind t0 x s2) H1))
         (ap (fun x => TBind t0 t1 x) H2)).
Qed.

Lemma congr_Univ {s0 : nat} {t0 : nat} (H0 : s0 = t0) : Univ s0 = Univ t0.
Proof.
exact (eq_trans eq_refl (ap (fun x => Univ x) H0)).
Qed.

Lemma congr_BVal {s0 : bool} {t0 : bool} (H0 : s0 = t0) : BVal s0 = BVal t0.
Proof.
exact (eq_trans eq_refl (ap (fun x => BVal x) H0)).
Qed.

Lemma congr_Bool : Bool = Bool.
Proof.
exact (eq_refl).
Qed.

Lemma congr_If {s0 : Tm} {s1 : Tm} {s2 : Tm} {t0 : Tm} {t1 : Tm} {t2 : Tm}
  (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : If s0 s1 s2 = If t0 t1 t2.
Proof.
exact (eq_trans
         (eq_trans (eq_trans eq_refl (ap (fun x => If x s1 s2) H0))
            (ap (fun x => If t0 x s2) H1)) (ap (fun x => If t0 t1 x) H2)).
Qed.

Lemma upRen_Tm_Tm (xi : nat -> nat) : nat -> nat.
Proof.
exact (up_ren xi).
Defined.

Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => VarTm (xi_Tm s0)
  | Abs s0 s1 => Abs (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1)
  | App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Pair s0 s1 => Pair (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Proj s0 s1 => Proj s0 (ren_Tm xi_Tm s1)
  | TBind s0 s1 s2 =>
      TBind s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2)
  | Univ s0 => Univ s0
  | BVal s0 => BVal s0
  | Bool => Bool
  | If s0 s1 s2 => If (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) (ren_Tm xi_Tm s2)
  end.

Lemma up_Tm_Tm (sigma : nat -> Tm) : nat -> Tm.
Proof.
exact (scons (VarTm var_zero) (funcomp (ren_Tm shift) sigma)).
Defined.

Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => sigma_Tm s0
  | Abs s0 s1 => Abs (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
  | App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Pair s0 s1 => Pair (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Proj s0 s1 => Proj s0 (subst_Tm sigma_Tm s1)
  | TBind s0 s1 s2 =>
      TBind s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
  | Univ s0 => Univ s0
  | BVal s0 => BVal s0
  | Bool => Bool
  | If s0 s1 s2 =>
      If (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) (subst_Tm sigma_Tm s2)
  end.

Lemma upId_Tm_Tm (sigma : nat -> Tm) (Eq : forall x, sigma x = VarTm x) :
  forall x, up_Tm_Tm sigma x = VarTm x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_Tm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm)
(Eq_Tm : forall x, sigma_Tm x = VarTm x) (s : Tm) {struct s} :
subst_Tm sigma_Tm s = s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (idSubst_Tm sigma_Tm Eq_Tm s0)
        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
        (idSubst_Tm sigma_Tm Eq_Tm s1)
  | Proj s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
        (idSubst_Tm sigma_Tm Eq_Tm s2)
  end.

Lemma upExtRen_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat)
  (Eq : forall x, xi x = zeta x) :
  forall x, upRen_Tm_Tm xi x = upRen_Tm_Tm zeta x.
Proof.
exact (fun n => match n with
                | S n' => ap shift (Eq n')
                | O => eq_refl
                end).
Qed.

Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
(Eq_Tm : forall x, xi_Tm x = zeta_Tm x) (s : Tm) {struct s} :
ren_Tm xi_Tm s = ren_Tm zeta_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
  | Abs s0 s1 =>
      congr_Abs (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
           (upExtRen_Tm_Tm _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
  | Proj s0 s1 => congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
        (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
           (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s2)
  end.

Lemma upExt_Tm_Tm (sigma : nat -> Tm) (tau : nat -> Tm)
  (Eq : forall x, sigma x = tau x) :
  forall x, up_Tm_Tm sigma x = up_Tm_Tm tau x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_Tm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
(Eq_Tm : forall x, sigma_Tm x = tau_Tm x) (s : Tm) {struct s} :
subst_Tm sigma_Tm s = subst_Tm tau_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
           s1)
  | App s0 s1 =>
      congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
  | Proj s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
        (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
           s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm sigma_Tm tau_Tm Eq_Tm s2)
  end.

Lemma up_ren_ren_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat)
  (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) :
  forall x, funcomp (upRen_Tm_Tm zeta) (upRen_Tm_Tm xi) x = upRen_Tm_Tm rho x.
Proof.
exact (up_ren_ren xi zeta rho Eq).
Qed.

Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
(rho_Tm : nat -> nat) (Eq_Tm : forall x, funcomp zeta_Tm xi_Tm x = rho_Tm x)
(s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
  | Abs s0 s1 =>
      congr_Abs (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
  | Proj s0 s1 =>
      congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
        (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s2)
  end.

Lemma up_ren_subst_Tm_Tm (xi : nat -> nat) (tau : nat -> Tm)
  (theta : nat -> Tm) (Eq : forall x, funcomp tau xi x = theta x) :
  forall x, funcomp (up_Tm_Tm tau) (upRen_Tm_Tm xi) x = up_Tm_Tm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_Tm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp tau_Tm xi_Tm x = theta_Tm x) (s : Tm) {struct s} :
subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
  | Proj s0 s1 =>
      congr_Proj (eq_refl s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
        (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s2)
  end.

Lemma up_subst_ren_Tm_Tm (sigma : nat -> Tm) (zeta_Tm : nat -> nat)
  (theta : nat -> Tm)
  (Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) :
  forall x,
  funcomp (ren_Tm (upRen_Tm_Tm zeta_Tm)) (up_Tm_Tm sigma) x =
  up_Tm_Tm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' =>
           eq_trans
             (compRenRen_Tm shift (upRen_Tm_Tm zeta_Tm)
                (funcomp shift zeta_Tm) (fun x => eq_refl) (sigma n'))
             (eq_trans
                (eq_sym
                   (compRenRen_Tm zeta_Tm shift (funcomp shift zeta_Tm)
                      (fun x => eq_refl) (sigma n')))
                (ap (ren_Tm shift) (Eq n')))
       | O => eq_refl
       end).
Qed.

Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (ren_Tm zeta_Tm) sigma_Tm x = theta_Tm x) 
(s : Tm) {struct s} :
ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
  | Proj s0 s1 =>
      congr_Proj (eq_refl s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
        (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s2)
  end.

Lemma up_subst_subst_Tm_Tm (sigma : nat -> Tm) (tau_Tm : nat -> Tm)
  (theta : nat -> Tm)
  (Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) :
  forall x,
  funcomp (subst_Tm (up_Tm_Tm tau_Tm)) (up_Tm_Tm sigma) x = up_Tm_Tm theta x.
Proof.
exact (fun n =>
       match n with
       | S n' =>
           eq_trans
             (compRenSubst_Tm shift (up_Tm_Tm tau_Tm)
                (funcomp (up_Tm_Tm tau_Tm) shift) (fun x => eq_refl)
                (sigma n'))
             (eq_trans
                (eq_sym
                   (compSubstRen_Tm tau_Tm shift
                      (funcomp (ren_Tm shift) tau_Tm) (fun x => eq_refl)
                      (sigma n'))) (ap (ren_Tm shift) (Eq n')))
       | O => eq_refl
       end).
Qed.

Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (subst_Tm tau_Tm) sigma_Tm x = theta_Tm x)
(s : Tm) {struct s} :
subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
  | Proj s0 s1 =>
      congr_Proj (eq_refl s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
        (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s2)
  end.

Lemma renRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) (s : Tm) :
  ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm (funcomp zeta_Tm xi_Tm) s.
Proof.
exact (compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.

Lemma renRen'_Tm_pointwise (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) :
  pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (ren_Tm xi_Tm))
    (ren_Tm (funcomp zeta_Tm xi_Tm)).
Proof.
exact (fun s => compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.

Lemma renSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) (s : Tm) :
  subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm (funcomp tau_Tm xi_Tm) s.
Proof.
exact (compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.

Lemma renSubst_Tm_pointwise (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) :
  pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (ren_Tm xi_Tm))
    (subst_Tm (funcomp tau_Tm xi_Tm)).
Proof.
exact (fun s => compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.

Lemma substRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) (s : Tm) :
  ren_Tm zeta_Tm (subst_Tm sigma_Tm s) =
  subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm) s.
Proof.
exact (compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.

Lemma substRen_Tm_pointwise (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) :
  pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (subst_Tm sigma_Tm))
    (subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm)).
Proof.
exact (fun s => compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.

Lemma substSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) (s : Tm) :
  subst_Tm tau_Tm (subst_Tm sigma_Tm s) =
  subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm) s.
Proof.
exact (compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.

Lemma substSubst_Tm_pointwise (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) :
  pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (subst_Tm sigma_Tm))
    (subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm)).
Proof.
exact (fun s => compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.

Lemma rinstInst_up_Tm_Tm (xi : nat -> nat) (sigma : nat -> Tm)
  (Eq : forall x, funcomp (VarTm) xi x = sigma x) :
  forall x, funcomp (VarTm) (upRen_Tm_Tm xi) x = up_Tm_Tm sigma x.
Proof.
exact (fun n =>
       match n with
       | S n' => ap (ren_Tm shift) (Eq n')
       | O => eq_refl
       end).
Qed.

Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (VarTm) xi_Tm x = sigma_Tm x) (s : Tm) {struct s}
   : ren_Tm xi_Tm s = subst_Tm sigma_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
  | Abs s0 s1 =>
      congr_Abs (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
  | Pair s0 s1 =>
      congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
  | Proj s0 s1 =>
      congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
  | TBind s0 s1 s2 =>
      congr_TBind (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
        (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
  | Univ s0 => congr_Univ (eq_refl s0)
  | BVal s0 => congr_BVal (eq_refl s0)
  | Bool => congr_Bool
  | If s0 s1 s2 =>
      congr_If (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s2)
  end.

Lemma rinstInst'_Tm (xi_Tm : nat -> nat) (s : Tm) :
  ren_Tm xi_Tm s = subst_Tm (funcomp (VarTm) xi_Tm) s.
Proof.
exact (rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
Qed.

Lemma rinstInst'_Tm_pointwise (xi_Tm : nat -> nat) :
  pointwise_relation _ eq (ren_Tm xi_Tm) (subst_Tm (funcomp (VarTm) xi_Tm)).
Proof.
exact (fun s => rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
Qed.

Lemma instId'_Tm (s : Tm) : subst_Tm (VarTm) s = s.
Proof.
exact (idSubst_Tm (VarTm) (fun n => eq_refl) s).
Qed.

Lemma instId'_Tm_pointwise : pointwise_relation _ eq (subst_Tm (VarTm)) id.
Proof.
exact (fun s => idSubst_Tm (VarTm) (fun n => eq_refl) s).
Qed.

Lemma rinstId'_Tm (s : Tm) : ren_Tm id s = s.
Proof.
exact (eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
Qed.

Lemma rinstId'_Tm_pointwise : pointwise_relation _ eq (@ren_Tm id) id.
Proof.
exact (fun s => eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
Qed.

Lemma varL'_Tm (sigma_Tm : nat -> Tm) (x : nat) :
  subst_Tm sigma_Tm (VarTm x) = sigma_Tm x.
Proof.
exact (eq_refl).
Qed.

Lemma varL'_Tm_pointwise (sigma_Tm : nat -> Tm) :
  pointwise_relation _ eq (funcomp (subst_Tm sigma_Tm) (VarTm)) sigma_Tm.
Proof.
exact (fun x => eq_refl).
Qed.

Lemma varLRen'_Tm (xi_Tm : nat -> nat) (x : nat) :
  ren_Tm xi_Tm (VarTm x) = VarTm (xi_Tm x).
Proof.
exact (eq_refl).
Qed.

Lemma varLRen'_Tm_pointwise (xi_Tm : nat -> nat) :
  pointwise_relation _ eq (funcomp (ren_Tm xi_Tm) (VarTm))
    (funcomp (VarTm) xi_Tm).
Proof.
exact (fun x => eq_refl).
Qed.

Class Up_Tm X Y :=
    up_Tm : X -> Y.

Class Up_PTm X Y :=
    up_PTm : X -> Y.

#[global] Instance Subst_Tm : (Subst1 _ _ _) := @subst_Tm.

#[global] Instance Up_Tm_Tm : (Up_Tm _ _) := @up_Tm_Tm.

#[global] Instance Ren_Tm : (Ren1 _ _ _) := @ren_Tm.

#[global] Instance VarInstance_Tm : (Var _ _) := @VarTm.

#[global] Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm.

#[global] Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm.

#[global] Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm.

#[global]
Instance VarInstance_PTm : (Var _ _) := @VarPTm.

Notation "[ sigma_Tm ]" := (subst_Tm sigma_Tm)
( at level 1, left associativity, only printing)  : fscope.

Notation "s [ sigma_Tm ]" := (subst_Tm sigma_Tm s)
( at level 7, left associativity, only printing)  : subst_scope.

Notation "↑__Tm" := up_Tm (only printing)  : subst_scope.

Notation "↑__Tm" := up_Tm_Tm (only printing)  : subst_scope.

Notation "⟨ xi_Tm ⟩" := (ren_Tm xi_Tm)
( at level 1, left associativity, only printing)  : fscope.

Notation "s ⟨ xi_Tm ⟩" := (ren_Tm xi_Tm s)
( at level 7, left associativity, only printing)  : subst_scope.

Notation "'var'" := VarTm ( at level 1, only printing)  : subst_scope.

Notation "x '__Tm'" := (@ids _ _ VarInstance_Tm x)
( at level 5, format "x __Tm", only printing)  : subst_scope.

Notation "x '__Tm'" := (VarTm x) ( at level 5, format "x __Tm")  :
subst_scope.

Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm)
( at level 1, left associativity, only printing)  : fscope.

Notation "s [ sigma_PTm ]" := (subst_PTm sigma_PTm s)
( at level 7, left associativity, only printing)  : subst_scope.

Notation "↑__PTm" := up_PTm (only printing)  : subst_scope.

Notation "↑__PTm" := up_PTm_PTm (only printing)  : subst_scope.

Notation "⟨ xi_PTm ⟩" := (ren_PTm xi_PTm)
( at level 1, left associativity, only printing)  : fscope.

Notation "s ⟨ xi_PTm ⟩" := (ren_PTm xi_PTm s)
( at level 7, left associativity, only printing)  : subst_scope.

Notation "'var'" := VarPTm ( at level 1, only printing)  : subst_scope.

Notation "x '__PTm'" := (@ids _ _ VarInstance_PTm x)
( at level 5, format "x __PTm", only printing)  : subst_scope.

Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm")  :
subst_scope.

#[global]
Instance subst_Tm_morphism :
 (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
    (@subst_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
       eq_ind s (fun t' => subst_Tm f_Tm s = subst_Tm g_Tm t')
         (ext_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
Qed.

#[global]
Instance subst_Tm_morphism2 :
 (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
    (@subst_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s => ext_Tm f_Tm g_Tm Eq_Tm s).
Qed.

#[global]
Instance ren_Tm_morphism :
 (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
       eq_ind s (fun t' => ren_Tm f_Tm s = ren_Tm g_Tm t')
         (extRen_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
Qed.

#[global]
Instance ren_Tm_morphism2 :
 (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
    (@ren_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s => extRen_Tm f_Tm g_Tm Eq_Tm s).
Qed.

#[global]
Instance subst_PTm_morphism :
 (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
    (@subst_PTm)).
Proof.
exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
       eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t')
         (ext_PTm f_PTm g_PTm Eq_PTm s) t Eq_st).
Qed.

#[global]
Instance subst_PTm_morphism2 :
 (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
    (@subst_PTm)).
Proof.
exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s).
Qed.

#[global]
Instance ren_PTm_morphism :
 (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_PTm)).
Proof.
exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
       eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t')
         (extRen_PTm f_PTm g_PTm Eq_PTm s) t Eq_st).
Qed.

#[global]
Instance ren_PTm_morphism2 :
 (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
    (@ren_PTm)).
Proof.
exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s).
Qed.

Ltac auto_unfold := repeat
                     unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1,
                      Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1,
                      VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, Up_Tm_Tm,
                      Up_Tm, up_Tm, Subst_Tm, Subst1, subst1.

Tactic Notation "auto_unfold" "in" "*" := repeat
                                           unfold VarInstance_PTm, Var, ids,
                                            Ren_PTm, Ren1, ren1, Up_PTm_PTm,
                                            Up_PTm, up_PTm, Subst_PTm,
                                            Subst1, subst1, VarInstance_Tm,
                                            Var, ids, Ren_Tm, Ren1, ren1,
                                            Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm,
                                            Subst1, subst1 in *.

Ltac asimpl' := repeat (first
                 [ progress setoid_rewrite substSubst_Tm_pointwise
                 | progress setoid_rewrite substSubst_Tm
                 | progress setoid_rewrite substRen_Tm_pointwise
                 | progress setoid_rewrite substRen_Tm
                 | progress setoid_rewrite renSubst_Tm_pointwise
                 | progress setoid_rewrite renSubst_Tm
                 | progress setoid_rewrite renRen'_Tm_pointwise
                 | progress setoid_rewrite renRen_Tm
                 | progress setoid_rewrite substSubst_PTm_pointwise
                 | progress setoid_rewrite substSubst_PTm
                 | progress setoid_rewrite substRen_PTm_pointwise
                 | progress setoid_rewrite substRen_PTm
                 | progress setoid_rewrite renSubst_PTm_pointwise
                 | progress setoid_rewrite renSubst_PTm
                 | progress setoid_rewrite renRen'_PTm_pointwise
                 | progress setoid_rewrite renRen_PTm
                 | progress setoid_rewrite varLRen'_Tm_pointwise
                 | progress setoid_rewrite varLRen'_Tm
                 | progress setoid_rewrite varL'_Tm_pointwise
                 | progress setoid_rewrite varL'_Tm
                 | progress setoid_rewrite rinstId'_Tm_pointwise
                 | progress setoid_rewrite rinstId'_Tm
                 | progress setoid_rewrite instId'_Tm_pointwise
                 | progress setoid_rewrite instId'_Tm
                 | progress setoid_rewrite varLRen'_PTm_pointwise
                 | progress setoid_rewrite varLRen'_PTm
                 | progress setoid_rewrite varL'_PTm_pointwise
                 | progress setoid_rewrite varL'_PTm
                 | progress setoid_rewrite rinstId'_PTm_pointwise
                 | progress setoid_rewrite rinstId'_PTm
                 | progress setoid_rewrite instId'_PTm_pointwise
                 | progress setoid_rewrite instId'_PTm
                 | progress
                    unfold up_Tm_Tm, upRen_Tm_Tm, up_PTm_PTm, upRen_PTm_PTm,
                     up_ren
                 | progress cbn[subst_Tm ren_Tm subst_PTm ren_PTm]
                 | progress fsimpl ]).

Ltac asimpl := check_no_evars;
                repeat
                 unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1,
                  Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1,
                  VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, Up_Tm_Tm,
                  Up_Tm, up_Tm, Subst_Tm, Subst1, subst1 in *; asimpl';
                minimize.

Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.

Tactic Notation "auto_case" := auto_case ltac:(asimpl; cbn; eauto).

Ltac substify := auto_unfold; try setoid_rewrite rinstInst'_Tm_pointwise;
                  try setoid_rewrite rinstInst'_Tm;
                  try setoid_rewrite rinstInst'_PTm_pointwise;
                  try setoid_rewrite rinstInst'_PTm.

Ltac renamify := auto_unfold; try setoid_rewrite_left rinstInst'_Tm_pointwise;
                  try setoid_rewrite_left rinstInst'_Tm;
                  try setoid_rewrite_left rinstInst'_PTm_pointwise;
                  try setoid_rewrite_left rinstInst'_PTm.

End Core.

Module Extra.

Import Core.

#[global] Hint Opaque subst_Tm: rewrite.

#[global] Hint Opaque ren_Tm: rewrite.

#[global] Hint Opaque subst_PTm: rewrite.

#[global] Hint Opaque ren_PTm: rewrite.

End Extra.

Module interface.

Export Core.

Export Extra.

End interface.

Export interface.