Top.SystemC.Infrastructure

The source of this file can be found on Github.

This file is a (more-or-less) straight forward adaptation of the infrastructure code that is necessary to work with locally nameless.

All lemmas and proofs are just concerned with binding and are not especially interesting.

Free Variables

Free Expression Variables

Fixpoint fv_ee (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i ⇒ {}
  | exp_fvar x ⇒ singleton x
  | exp_const ⇒ {}
  | exp_box C b ⇒ fv_eb b
  end
with fv_es (s : stm) {struct s} : atoms :=
  match s with
  | stm_ret e ⇒ fv_ee e
  | stm_val T s1 s2 ⇒ (fv_es s1) `union` (fv_es s2)
  | stm_def C S1 b s ⇒ (fv_eb b) `union` (fv_es s)
  | stm_vapp b e ⇒ (fv_eb b) `union` (fv_ee e)
  | stm_bapp b C g ⇒ (fv_eb b) `union` (fv_eb g)
  | stm_try C T1 T b g ⇒ (fv_es b) `union` (fv_es g)
  | stm_reset l C b g ⇒ (fv_es b) `union` (fv_es g)
  | stm_perform b e ⇒ fv_eb b `union` fv_ee e
  end
with fv_eb (b : blk) {struct b} : atoms :=
  match b with
  | blk_bvar i ⇒ {}
  | blk_fvar x ⇒ {}
  | blk_vabs T s ⇒ fv_es s
  | blk_babs S1 s ⇒ fv_es s
  | blk_tabs s ⇒ fv_eb s
  | blk_tapp s T ⇒ fv_eb s
  | blk_unbox e ⇒ fv_ee e
  | blk_handler l ⇒ {}
  end.

Free Block Term Variables

Fixpoint fv_be (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i ⇒ {}
  | exp_fvar x ⇒ {}
  | exp_const ⇒ {}
  | exp_box C1 b ⇒ fv_bb b
  end
with fv_bs (s : stm) {struct s} : atoms :=
  match s with
  | stm_ret e ⇒ fv_be e
  | stm_val T s1 s2 ⇒ (fv_bs s1) `union` (fv_bs s2)
  | stm_def C1 S1 b s ⇒ (fv_bb b) `union` (fv_bs s)
  | stm_vapp b e ⇒ (fv_bb b) `union` (fv_be e)
  | stm_bapp b C1 g ⇒ (fv_bb b) `union` (fv_bb g)
  | stm_try C T1 T b g ⇒ (fv_bs b) `union` (fv_bs g)
  | stm_reset l C b g ⇒ (fv_bs b) `union` (fv_bs g)
  | stm_perform b e ⇒ fv_bb b `union` fv_be e
  end
with fv_bb (b : blk) {struct b} : atoms :=
  match b with
  | blk_bvar i ⇒ {}
  | blk_fvar x ⇒ (singleton x)
  | blk_vabs T s ⇒ (fv_bs s)
  | blk_babs S1 s ⇒ (fv_bs s)
  | blk_tabs s ⇒ fv_bb s
  | blk_tapp s T ⇒ fv_bb s
  | blk_unbox e ⇒ (fv_be e)
  | blk_handler l ⇒ {}
  end.

Free Block Type Variables

Fixpoint fv_cvt (T : vtyp) {struct T} : atoms :=
  match T with
  | typ_base ⇒ {}
  | typ_capt S1 C1 ⇒ (fv_cbt S1) `union` (cset_fvars C1)
  | typ_fvar a ⇒ {}
  | typ_bvar n ⇒ {}
  end
with fv_cbt (S1 : btyp) {struct S1} : atoms :=
  match S1 with
  | typ_vfun T1 T2 ⇒ (fv_cvt T1) `union` (fv_cvt T2)
  | typ_bfun S1 T ⇒ (fv_cbt S1) `union` (fv_cvt T)
  | typ_eff T1 T ⇒ (fv_cvt T1) `union` (fv_cvt T)
  | typ_tfun T ⇒ (fv_cbt T)
  end.

Fixpoint fv_ce (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i ⇒ {}
  | exp_fvar x ⇒ {}
  | exp_const ⇒ {}
  | exp_box C1 b ⇒ (cset_fvars C1) `union` (fv_cb b)
  end

with fv_cs (s : stm) {struct s} : atoms :=
  match s with
  | stm_ret e ⇒ (fv_ce e)
  | stm_val T s1 s2 ⇒ (fv_cvt T) `union` (fv_cs s1) `union` (fv_cs s2)
  | stm_def C1 S1 b s ⇒ (cset_fvars C1) `union` (fv_cbt S1) `union` (fv_cb b) `union` (fv_cs s)
  | stm_vapp b e ⇒ (fv_cb b) `union` (fv_ce e)
  | stm_bapp b C1 g ⇒ (fv_cb b) `union` (cset_fvars C1) `union` (fv_cb g)
  | stm_try C1 T1 T b g ⇒ (fv_cvt T1) `union` (fv_cvt T) `union` (cset_fvars C1) `union` (fv_cs b) `union` (fv_cs g)
  | stm_reset l C1 b g ⇒ (cset_fvars C1) `union` (fv_cs b) `union` (fv_cs g)
  | stm_perform b e ⇒ fv_cb b `union` fv_ce e
  end

with fv_cb (b : blk) {struct b} : atoms :=
  match b with
  | blk_bvar i ⇒ {}
  | blk_fvar x ⇒ singleton x
  | blk_vabs T s ⇒ (fv_cvt T) `union` (fv_cs s)
  | blk_babs S1 s ⇒ (fv_cbt S1) `union` (fv_cs s)
  | blk_tabs s ⇒ (fv_cb s)
  | blk_tapp s T ⇒ (fv_cb s) `union` (fv_cvt T)
  | blk_unbox e ⇒ (fv_ce e)
  | blk_handler l ⇒ {}
  end.

Free Type Variables

Fixpoint fv_tvt (T : vtyp) {struct T} : atoms :=
match T with
  | typ_base ⇒ {}
  | typ_capt S1 C1 ⇒ (fv_tbt S1)
  | typ_fvar a ⇒ singleton a
  | typ_bvar n ⇒ {}
  end
with fv_tbt (S1 : btyp) {struct S1} : atoms :=
  match S1 with
  | typ_vfun T1 T2 ⇒ (fv_tvt T1) `union` (fv_tvt T2)
  | typ_bfun S1 T ⇒ (fv_tbt S1) `union` (fv_tvt T)
  | typ_eff T1 T ⇒ (fv_tvt T1) `union` (fv_tvt T)
  | typ_tfun T ⇒ (fv_tbt T)
  end.

Fixpoint fv_te (e : exp) {struct e} : atoms :=
  match e with
  | exp_bvar i ⇒ {}
  | exp_fvar x ⇒ {}
  | exp_const ⇒ {}
  | exp_box C b ⇒ fv_tb b
  end
with fv_ts (s : stm) {struct s} : atoms :=
  match s with
  | stm_ret e ⇒ fv_te e
  | stm_val T s1 s2 ⇒ (fv_tvt T) `union` (fv_ts s1) `union` (fv_ts s2)
  | stm_def C S1 b s ⇒ (fv_tbt S1) `union` (fv_tb b) `union` (fv_ts s)
  | stm_vapp b e ⇒ (fv_tb b) `union` (fv_te e)
  | stm_bapp b C g ⇒ (fv_tb b) `union` (fv_tb g)
  | stm_try C T1 T b g ⇒ (fv_tvt T1) `union` (fv_tvt T) `union` (fv_ts b) `union` (fv_ts g)
  | stm_reset l C b g ⇒ (fv_ts b) `union` (fv_ts g)
  | stm_perform b e ⇒ fv_tb b `union` fv_te e
  end
with fv_tb (b : blk) {struct b} : atoms :=
  match b with
  | blk_bvar i ⇒ {}
  | blk_fvar x ⇒ {}
  | blk_vabs T s ⇒ fv_tvt T `union` fv_ts s
  | blk_babs S1 s ⇒ fv_tbt S1 `union` fv_ts s
  | blk_tabs s ⇒ fv_tb s
  | blk_tapp s T ⇒ fv_tvt T `union` fv_tb s
  | blk_unbox e ⇒ fv_te e
  | blk_handler l ⇒ {}
  end.

Definition fv_bbind (b : binding) : atoms :=
  match b with
  | bind_val T ⇒ {}
  | bind_blk s tracked ⇒ (fv_cbt s)
  | bind_blk s (capture C2) ⇒ (fv_cbt s) `union` (cset_fvars C2)
  | bind_typ ⇒ {}
  end.

The second step in defining "pick fresh" is to define the tactic itself. It is based on the (pick fresh ... for ...) tactic defined in the Atom library. Here, we use gather_atoms to construct the set L rather than leaving it to the user to provide. Thus, invoking (pick fresh x) introduces a new atom x into the current context that is fresh for "everything" in the context.

Tactic Notation "pick" "fresh" ident(x) :=
  let L := gather_atoms in (pick fresh x for L).

The "pick fresh and apply" tactic

This tactic is implementation specific only because of its reliance on gather_atoms, which is itself implementation specific. The definition below may be copied between developments without any changes, assuming that the other other developments define an appropriate gather_atoms tactic. For documentation on the tactic on which the one below is based, see the Metatheory library.

Tactic Notation
      "pick" "fresh" ident(atom_name) "and" "apply" constr(lemma) :=
  let L := gather_atoms in
  pick fresh atom_name excluding L and apply lemma.

Lemma subst_ee_intro_rec : ∀ x e u k,
  x `notin` fv_ee e →
  open_ee_rec k u e = subst_ee x u (open_ee_rec k (exp_fvar x) e)
with subst_es_intro_rec : ∀ x e u k,
  x `notin` fv_es e →
  open_es_rec k u e = subst_es x u (open_es_rec k (exp_fvar x) e)
with subst_eb_intro_rec : ∀ x e u k,
  x `notin` fv_eb e →
  open_eb_rec k u e = subst_eb x u (open_eb_rec k (exp_fvar x) e).

Lemma subst_ee_intro : ∀ x e u,
  x `notin` fv_ee e →
  open_ee e u = subst_ee x u (open_ee e x)
with subst_es_intro : ∀ x e u,
  x `notin` fv_es e →
  open_es e u = subst_es x u (open_es e x)
with subst_eb_intro : ∀ x e u,
  x `notin` fv_eb e →
  open_eb e u = subst_eb x u (open_eb e x).

Lemma subst_be_intro_rec : ∀ x e u k,
  x `notin` fv_be e →
  open_be_rec k u e = subst_be x u (open_be_rec k (blk_fvar x) e)
with subst_bs_intro_rec : ∀ x e u k,
  x `notin` fv_bs e →
  open_bs_rec k u e = subst_bs x u (open_bs_rec k (blk_fvar x) e)
with subst_bb_intro_rec : ∀ x e u k,
  x `notin` fv_bb e →
  open_bb_rec k u e = subst_bb x u (open_bb_rec k (blk_fvar x) e).

Lemma subst_be_intro : ∀ x e u,
  x `notin` fv_be e →
  open_be e u = subst_be x u (open_be e x)
with subst_bs_intro : ∀ x e u,
  x `notin` fv_bs e →
  open_bs e u = subst_bs x u (open_bs e x)
with subst_bb_intro : ∀ x e u,
  x `notin` fv_bb e →
  open_bb e u = subst_bb x u (open_bb e x).

Lemma subst_cvt_intro_rec : ∀ X T2 U k,
  X `notin` fv_cvt T2 →
  open_cvt_rec k U T2 = subst_cvt X U (open_cvt_rec k (cset_fvar X) T2)
with subst_cbt_intro_rec : ∀ X T2 U k,
  X `notin` fv_cbt T2 →
  open_cbt_rec k U T2 = subst_cbt X U (open_cbt_rec k (cset_fvar X) T2).

Lemma subst_cvt_intro : ∀ X T2 U,
  X `notin` fv_cvt T2 →
  open_cvt T2 U = subst_cvt X U (open_cvt T2 (cset_fvar X))
with subst_cbt_intro : ∀ X T2 U,
  X `notin` fv_cbt T2 →
  open_cbt T2 U = subst_cbt X U (open_cbt T2 (cset_fvar X)).

Lemma subst_ce_intro_rec : ∀ x e u C k,
  x `notin` fv_ce e →
  open_ce_rec k u C e = subst_ce x u C (open_ce_rec k x (cset_fvar x) e)
with subst_cs_intro_rec : ∀ x e u C k,
  x `notin` fv_cs e →
  open_cs_rec k u C e = subst_cs x u C (open_cs_rec k x (cset_fvar x) e)
with subst_cb_intro_rec : ∀ x e u C k,
  x `notin` fv_cb e →
  open_cb_rec k u C e = subst_cb x u C (open_cb_rec k x (cset_fvar x) e).

Lemma subst_ce_intro : ∀ x e u C,
  x `notin` fv_ce e →
  open_ce e u C = subst_ce x u C (open_ce e x (cset_fvar x))
with subst_cs_intro : ∀ x e u C,
  x `notin` fv_cs e →
  open_cs e u C = subst_cs x u C (open_cs e x (cset_fvar x))
with subst_cb_intro : ∀ x e u C,
  x `notin` fv_cb e →
  open_cb e u C = subst_cb x u C (open_cb e x (cset_fvar x)).

Opening Closed Lemmas

The naming scheme of the aux lemmas is:

    open_EXPRe_rec j u e = open_CE_rec i P C (open_EXPR_rec j u e)

Lemma open_cvt_rec_capt_aux : ∀ T j V i U,
  i ≠ j →
  capt V →
  (cset_fvars V) `disjoint` (cset_fvars U) →
  labels_disjoint (cset_lvars V) (cset_lvars U) →
  open_cvt_rec j V T = open_cvt_rec i U (open_cvt_rec j V T) →
  T = open_cvt_rec i U T
with open_cbt_rec_capt_aux : ∀ T j V i U,
  i ≠ j →
  capt V →
  (cset_fvars V) `disjoint` (cset_fvars U) →
  labels_disjoint (cset_lvars V) (cset_lvars U) →
  open_cbt_rec j V T = open_cbt_rec i U (open_cbt_rec j V T) →
  T = open_cbt_rec i U T.

Lemma open_cvt_rec_type_aux : ∀ T j U i C,
  open_tvt_rec j U T = open_cvt_rec i C (open_tvt_rec j U T) →
  T = open_cvt_rec i C T
with open_cbt_rec_type_aux : ∀ T j U i C,
  open_tbt_rec j U T = open_cbt_rec i C (open_tbt_rec j U T) →
  T = open_cbt_rec i C T.

Lemma open_cvt_rec_vtype : ∀ T U k,
  vtype T →
  T = open_cvt_rec k U T
with open_cbt_rec_btype : ∀ T U k,
  btype T →
  T = open_cbt_rec k U T.

Lemma open_ee_rec_expr_aux : ∀ e j v u i,
  i ≠ j →
  open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) →
  e = open_ee_rec i u e
with open_eb_rec_expr_aux : ∀ e j v u i,
  i ≠ j →
  open_eb_rec j v e = open_eb_rec i u (open_eb_rec j v e) →
  e = open_eb_rec i u e
with open_es_rec_expr_aux : ∀ e j v u i,
  i ≠ j →
  open_es_rec j v e = open_es_rec i u (open_es_rec j v e) →
  e = open_es_rec i u e.

Lemma open_ce_rec_capt_aux : ∀ e j v u i (C D : cap),
  i ≠ j →
  capt C →
  (cset_fvars C) `disjoint` (cset_fvars D) →
  labels_disjoint (cset_lvars C) (cset_lvars D) →
  open_ce_rec j v C e = open_ce_rec i u D (open_ce_rec j v C e) →
  e = open_ce_rec i u D e
with open_cb_rec_capt_aux : ∀ e j v u i (C D : cap),
  i ≠ j →
  capt C →
  (cset_fvars C) `disjoint` (cset_fvars D) →
  labels_disjoint (cset_lvars C) (cset_lvars D) →
  open_cb_rec j v C e = open_cb_rec i u D (open_cb_rec j v C e) →
  e = open_cb_rec i u D e
with open_cs_rec_capt_aux : ∀ e j v u i (C D : cap),
  i ≠ j →
  capt C →
  (cset_fvars C) `disjoint` (cset_fvars D) →
  labels_disjoint (cset_lvars C) (cset_lvars D) →
  open_cs_rec j v C e = open_cs_rec i u D (open_cs_rec j v C e) →
  e = open_cs_rec i u D e.

Lemma open_ce_rec_expr_aux : ∀ e j u C i P ,
  open_ee_rec j u e = open_ce_rec i P C (open_ee_rec j u e) →
  e = open_ce_rec i P C e
with open_cb_rec_expr_aux : ∀ e j u C i P ,
  open_eb_rec j u e = open_cb_rec i P C (open_eb_rec j u e) →
  e = open_cb_rec i P C e
with open_cs_rec_expr_aux : ∀ e j u C i P ,
  open_es_rec j u e = open_cs_rec i P C (open_es_rec j u e) →
  e = open_cs_rec i P C e.

Lemma open_ce_rec_type_aux : ∀ e j u C i P ,
  open_te_rec j u e = open_ce_rec i P C (open_te_rec j u e) →
  e = open_ce_rec i P C e
with open_cb_rec_type_aux : ∀ e j u C i P ,
  open_tb_rec j u e = open_cb_rec i P C (open_tb_rec j u e) →
  e = open_cb_rec i P C e
with open_cs_rec_type_aux : ∀ e j u C i P ,
  open_ts_rec j u e = open_cs_rec i P C (open_ts_rec j u e) →
  e = open_cs_rec i P C e.

Lemma open_ee_rec_type_aux : ∀ e j U i f,
  open_te_rec j U e = open_ee_rec i f (open_te_rec j U e) →
  e = open_ee_rec i f e
with open_eb_rec_type_aux : ∀ e j U i f,
  open_tb_rec j U e = open_eb_rec i f (open_tb_rec j U e) →
  e = open_eb_rec i f e
with open_es_rec_type_aux : ∀ e j U i f,
  open_ts_rec j U e = open_es_rec i f (open_ts_rec j U e) →
  e = open_es_rec i f e.

Lemma open_be_rec_type_aux : ∀ e j U i f,
  open_te_rec j U e = open_be_rec i f (open_te_rec j U e) →
  e = open_be_rec i f e
with open_bb_rec_type_aux : ∀ e j U i f,
  open_tb_rec j U e = open_bb_rec i f (open_tb_rec j U e) →
  e = open_bb_rec i f e
with open_bs_rec_type_aux : ∀ e j U i f,
  open_ts_rec j U e = open_bs_rec i f (open_ts_rec j U e) →
  e = open_bs_rec i f e.

Lemma open_be_rec_expr_aux : ∀ e j u i P,
  open_ee_rec j u e = open_be_rec i P (open_ee_rec j u e) →
  e = open_be_rec i P e
with open_bb_rec_expr_aux : ∀ e j u i P ,
  open_eb_rec j u e = open_bb_rec i P (open_eb_rec j u e) →
  e = open_bb_rec i P e
with open_bs_rec_expr_aux : ∀ e j u i P ,
  open_es_rec j u e = open_bs_rec i P (open_es_rec j u e) →
  e = open_bs_rec i P e.

Lemma open_ce_rec_block_aux : ∀ e j u C i P,
  i ≠ j →
  open_be_rec j u e = open_ce_rec i P C (open_be_rec j u e) →
  e = open_ce_rec i P C e
with open_cb_rec_block_aux : ∀ e j u C i P,
  i ≠ j →
  open_bb_rec j u e = open_cb_rec i P C (open_bb_rec j u e) →
  e = open_cb_rec i P C e
with open_cs_rec_block_aux : ∀ e j u C i P,
  i ≠ j →
  open_bs_rec j u e = open_cs_rec i P C (open_bs_rec j u e) →
  e = open_cs_rec i P C e.

Lemma open_be_rec_capt_aux : ∀ e j u C i P,
  i ≠ j →
  open_ce_rec j u C e = open_be_rec i P (open_ce_rec j u C e) →
  e = open_be_rec i P e
with open_bb_rec_capt_aux : ∀ e j u C i P,
  i ≠ j →
  open_cb_rec j u C e = open_bb_rec i P (open_cb_rec j u C e) →
  e = open_bb_rec i P e
with open_bs_rec_capt_aux : ∀ e j u C i P,
  i ≠ j →
  open_cs_rec j u C e = open_bs_rec i P (open_cs_rec j u C e) →
  e = open_bs_rec i P e.

Lemma open_be_rec_block_aux : ∀ e j u i P,
  i ≠ j →
  open_be_rec j u e = open_be_rec i P (open_be_rec j u e) →
  e = open_be_rec i P e
with open_bb_rec_block_aux : ∀ e j u i P,
  i ≠ j →
  open_bb_rec j u e = open_bb_rec i P (open_bb_rec j u e) →
  e = open_bb_rec i P e
with open_bs_rec_block_aux : ∀ e j u i P,
  i ≠ j →
  open_bs_rec j u e = open_bs_rec i P (open_bs_rec j u e) →
  e = open_bs_rec i P e.

Lemma open_ee_rec_capt_aux : ∀ e j D u i P ,
  open_ce_rec j D u e = open_ee_rec i P (open_ce_rec j D u e) →
  e = open_ee_rec i P e
with open_eb_rec_capt_aux : ∀ e j D u i P ,
  open_cb_rec j D u e = open_eb_rec i P (open_cb_rec j D u e) →
  e = open_eb_rec i P e
with open_es_rec_capt_aux : ∀ e j D u i P ,
  open_cs_rec j D u e = open_es_rec i P (open_cs_rec j D u e) →
  e = open_es_rec i P e.

Lemma open_ee_rec_block_aux : ∀ e j u i P ,
  open_be_rec j u e = open_ee_rec i P (open_be_rec j u e) →
  e = open_ee_rec i P e
with open_eb_rec_block_aux : ∀ e j u i P ,
  open_bb_rec j u e = open_eb_rec i P (open_bb_rec j u e) →
  e = open_eb_rec i P e
with open_es_rec_block_aux : ∀ e j u i P ,
  open_bs_rec j u e = open_es_rec i P (open_bs_rec j u e) →
  e = open_es_rec i P e.

Lemma open_ce_rec_expr : ∀ e U C k,
  expr e →
  e = open_ce_rec k U C e
with open_cb_rec_block : ∀ e U C k,
  block e →
  e = open_cb_rec k U C e
with open_cs_rec_stmt : ∀ e U C k,
  stmt e →
  e = open_cs_rec k U C e.

Lemma open_ee_rec_expr : ∀ e U k,
  expr e →
  e = open_ee_rec k U e
with open_eb_rec_block : ∀ e U k,
  block e →
  e = open_eb_rec k U e
with open_es_rec_stmt : ∀ e U k,
  stmt e →
  e = open_es_rec k U e.

Lemma open_be_rec_expr : ∀ e U k,
  expr e →
  e = open_be_rec k U e
with open_bb_rec_block : ∀ e U k,
  block e →
  e = open_bb_rec k U e
with open_bs_rec_stmt : ∀ e U k,
  stmt e →
  e = open_bs_rec k U e.

Substitution / Opening Lemmas

Lemma subst_ee_open_ee_rec : ∀ e1 e2 x u k,
  expr u →
  subst_ee x u (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_ee x u e2) (subst_ee x u e1)
with subst_eb_open_eb_rec : ∀ e1 e2 x u k,
  expr u →
  subst_eb x u (open_eb_rec k e2 e1) =
    open_eb_rec k (subst_ee x u e2) (subst_eb x u e1)
with subst_es_open_es_rec : ∀ e1 e2 x u k,
  expr u →
  subst_es x u (open_es_rec k e2 e1) =
    open_es_rec k (subst_ee x u e2) (subst_es x u e1).

Lemma subst_ee_open_ee : ∀ e1 e2 x u,
  expr u →
  subst_ee x u (open_ee e1 e2) =
    open_ee (subst_ee x u e1) (subst_ee x u e2)
with subst_eb_open_eb : ∀ e1 e2 x u,
  expr u →
  subst_eb x u (open_eb e1 e2) =
    open_eb (subst_eb x u e1) (subst_ee x u e2)
with subst_es_open_es : ∀ e1 e2 x u,
  expr u →
  subst_es x u (open_es e1 e2) =
    open_es (subst_es x u e1) (subst_ee x u e2).

Lemma subst_ee_open_ee_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_ee (subst_ee x u e) y = subst_ee x u (open_ee e y)
with subst_eb_open_eb_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_eb (subst_eb x u e) y = subst_eb x u (open_eb e y)
with subst_es_open_es_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_es (subst_es x u e) y = subst_es x u (open_es e y).

Lemma subst_ee_open_ce_rec : ∀ e f C x u k,
  expr u →
  subst_ee x u (open_ce_rec k f C e) =
    open_ce_rec k (subst_eb x u f) C (subst_ee x u e)
with subst_eb_open_cb_rec : ∀ e f C x u k,
  expr u →
  subst_eb x u (open_cb_rec k f C e) =
    open_cb_rec k (subst_eb x u f) C (subst_eb x u e)
with subst_es_open_cs_rec : ∀ e f C x u k,
  expr u →
  subst_es x u (open_cs_rec k f C e) =
    open_cs_rec k (subst_eb x u f) C (subst_es x u e).

Lemma subst_ee_open_ce : ∀ e f C x u,
  expr u →
  subst_ee x u (open_ce e f C) = open_ce (subst_ee x u e) (subst_eb x u f) C
with subst_eb_open_cb : ∀ e f C x u,
  expr u →
  subst_eb x u (open_cb e f C) = open_cb (subst_eb x u e) (subst_eb x u f) C
with subst_es_open_cs : ∀ e f C x u,
  expr u →
  subst_es x u (open_cs e f C) = open_cs (subst_es x u e) (subst_eb x u f) C.

Lemma subst_ee_open_ce_var : ∀ e x (y : atom) u,
  expr u →
  open_ce (subst_ee x u e) y (cset_fvar y) = subst_ee x u (open_ce e y (cset_fvar y))
with subst_eb_open_cb_var : ∀ e x (y : atom) u,
  expr u →
  open_cb (subst_eb x u e) y (cset_fvar y) = subst_eb x u (open_cb e y (cset_fvar y))
with subst_es_open_cs_var : ∀ e x (y : atom) u,
  expr u →
  open_cs (subst_es x u e) y (cset_fvar y) = subst_es x u (open_cs e y (cset_fvar y)).

Lemma subst_ee_open_be_rec : ∀ e f x u k,
  expr u →
  subst_ee x u (open_be_rec k f e) =
    open_be_rec k (subst_eb x u f) (subst_ee x u e)
with subst_eb_open_bb_rec : ∀ e f x u k,
  expr u →
  subst_eb x u (open_bb_rec k f e) =
    open_bb_rec k (subst_eb x u f) (subst_eb x u e)
with subst_es_open_bs_rec : ∀ e f x u k,
  expr u →
  subst_es x u (open_bs_rec k f e) =
    open_bs_rec k (subst_eb x u f) (subst_es x u e).

Lemma subst_ee_open_be : ∀ e f x u,
  expr u →
  subst_ee x u (open_be e f) = open_be (subst_ee x u e) (subst_eb x u f)
with subst_eb_open_bb : ∀ e f x u,
  expr u →
  subst_eb x u (open_bb e f) = open_bb (subst_eb x u e) (subst_eb x u f)
with subst_es_open_bs : ∀ e f x u,
  expr u →
  subst_es x u (open_bs e f) = open_bs (subst_es x u e) (subst_eb x u f).

Lemma subst_ee_open_be_var : ∀ e x (y : atom) u,
  expr u →
  open_be (subst_ee x u e) y = subst_ee x u (open_be e y)
with subst_eb_open_bb_var : ∀ e x (y : atom) u,
  expr u →
  open_bb (subst_eb x u e) y = subst_eb x u (open_bb e y)
with subst_es_open_bs_var : ∀ e x (y : atom) u,
  expr u →
  open_bs (subst_es x u e) y = subst_es x u (open_bs e y).

Lemma subst_be_open_ee_rec : ∀ e1 e2 Z P k,
  block P →
  subst_be Z P (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_be Z P e2) (subst_be Z P e1)
with subst_bb_open_eb_rec : ∀ e1 e2 Z P k,
  block P →
  subst_bb Z P (open_eb_rec k e2 e1) =
    open_eb_rec k (subst_be Z P e2) (subst_bb Z P e1)
with subst_bs_open_es_rec : ∀ e1 e2 Z P k,
  block P →
  subst_bs Z P (open_es_rec k e2 e1) =
    open_es_rec k (subst_be Z P e2) (subst_bs Z P e1).

Lemma subst_be_open_ee : ∀ e1 e2 Z P,
  block P →
  subst_be Z P (open_ee e1 e2) = open_ee (subst_be Z P e1) (subst_be Z P e2)
with subst_bb_open_eb : ∀ e1 e2 Z P,
  block P →
  subst_bb Z P (open_eb e1 e2) = open_eb (subst_bb Z P e1) (subst_be Z P e2)
with subst_bs_open_es : ∀ e1 e2 Z P,
  block P →
  subst_bs Z P (open_es e1 e2) = open_es (subst_bs Z P e1) (subst_be Z P e2).

Lemma subst_be_open_ee_var : ∀ Z (x:atom) P e,
  block P →
  open_ee (subst_be Z P e) x = subst_be Z P (open_ee e x)
with subst_bb_open_eb_var : ∀ Z (x:atom) P e,
  block P →
  open_eb (subst_bb Z P e) x = subst_bb Z P (open_eb e x)
with subst_bs_open_es_var : ∀ Z (x:atom) P e,
  block P →
  open_es (subst_bs Z P e) x = subst_bs Z P (open_es e x).

Lemma subst_be_open_be_rec : ∀ e1 e2 Z P k,
  block P →
  subst_be Z P (open_be_rec k e2 e1) =
    open_be_rec k (subst_bb Z P e2) (subst_be Z P e1)
with subst_bb_open_bb_rec : ∀ e1 e2 Z P k,
  block P →
  subst_bb Z P (open_bb_rec k e2 e1) =
    open_bb_rec k (subst_bb Z P e2) (subst_bb Z P e1)
with subst_bs_open_bs_rec : ∀ e1 e2 Z P k,
  block P →
  subst_bs Z P (open_bs_rec k e2 e1) =
    open_bs_rec k (subst_bb Z P e2) (subst_bs Z P e1).

Lemma subst_be_open_be : ∀ e1 e2 Z P,
  block P →
  subst_be Z P (open_be e1 e2) = open_be (subst_be Z P e1) (subst_bb Z P e2)
with subst_bb_open_bb : ∀ e1 e2 Z P,
  block P →
  subst_bb Z P (open_bb e1 e2) = open_bb (subst_bb Z P e1) (subst_bb Z P e2)
with subst_bs_open_bs : ∀ e1 e2 Z P,
  block P →
  subst_bs Z P (open_bs e1 e2) = open_bs (subst_bs Z P e1) (subst_bb Z P e2).

Lemma subst_be_open_be_var : ∀ Z (x:atom) P e,
  Z ≠ x →
  block P →
  open_be (subst_be Z P e) x = subst_be Z P (open_be e x)
with subst_bb_open_bb_var : ∀ Z (x:atom) P e,
  Z ≠ x →
  block P →
  open_bb (subst_bb Z P e) x = subst_bb Z P (open_bb e x)
with subst_bs_open_bs_var : ∀ Z (x:atom) P e,
  Z ≠ x →
  block P →
  open_bs (subst_bs Z P e) x = subst_bs Z P (open_bs e x).

Lemma subst_ce_open_ee_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_ce Z P C (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_ce Z P C e2) (subst_ce Z P C e1)
with subst_cb_open_eb_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_cb Z P C (open_eb_rec k e2 e1) =
    open_eb_rec k (subst_ce Z P C e2) (subst_cb Z P C e1)
with subst_cs_open_es_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_cs Z P C (open_es_rec k e2 e1) =
    open_es_rec k (subst_ce Z P C e2) (subst_cs Z P C e1).

Lemma subst_ce_open_ee : ∀ e1 e2 Z P C,
  block P →
  subst_ce Z P C (open_ee e1 e2) = open_ee (subst_ce Z P C e1) (subst_ce Z P C e2)
with subst_cb_open_eb : ∀ e1 e2 Z P C,
  block P →
  subst_cb Z P C (open_eb e1 e2) = open_eb (subst_cb Z P C e1) (subst_ce Z P C e2)
with subst_cs_open_es : ∀ e1 e2 Z P C,
  block P →
  subst_cs Z P C (open_es e1 e2) = open_es (subst_cs Z P C e1) (subst_ce Z P C e2).

Lemma subst_ce_open_ee_var : ∀ Z (x:atom) P C e,
  block P →
  open_ee (subst_ce Z P C e) x = subst_ce Z P C (open_ee e x)
with subst_cb_open_eb_var : ∀ Z (x:atom) P C e,
  block P →
  open_eb (subst_cb Z P C e) x = subst_cb Z P C (open_eb e x)
with subst_cs_open_es_var : ∀ Z (x:atom) P C e,
  block P →
  open_es (subst_cs Z P C e) x = subst_cs Z P C (open_es e x).

Lemma subst_be_open_ce_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_be Z P (open_ce_rec k e2 C e1) =
    open_ce_rec k (subst_bb Z P e2) C (subst_be Z P e1)
with subst_bb_open_cb_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_bb Z P (open_cb_rec k e2 C e1) =
    open_cb_rec k (subst_bb Z P e2) C (subst_bb Z P e1)
with subst_bs_open_cs_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_bs Z P (open_cs_rec k e2 C e1) =
    open_cs_rec k (subst_bb Z P e2) C (subst_bs Z P e1).

Lemma subst_be_open_ce : ∀ e1 e2 Z P C,
  block P →
  subst_be Z P (open_ce e1 e2 C) = open_ce (subst_be Z P e1) (subst_bb Z P e2) C
with subst_bb_open_cb : ∀ e1 e2 Z P C,
  block P →
  subst_bb Z P (open_cb e1 e2 C) = open_cb (subst_bb Z P e1) (subst_bb Z P e2) C
with subst_bs_open_cs : ∀ e1 e2 Z P C,
  block P →
  subst_bs Z P (open_cs e1 e2 C) = open_cs (subst_bs Z P e1) (subst_bb Z P e2) C.

Lemma subst_be_open_ce_var : ∀ Z (x:atom) P e,
  block P →
  x ≠ Z →
  open_ce (subst_be Z P e) x (cset_fvar x) = subst_be Z P (open_ce e x (cset_fvar x))
with subst_bb_open_cb_var : ∀ Z (x:atom) P e,
  block P →
  x ≠ Z →
  open_cb (subst_bb Z P e) x (cset_fvar x) = subst_bb Z P (open_cb e x (cset_fvar x))
with subst_bs_open_cs_var : ∀ Z (x:atom) P e,
  block P →
  x ≠ Z →
  open_cs (subst_bs Z P e) x (cset_fvar x) = subst_bs Z P (open_cs e x (cset_fvar x)).

Lemma subst_ce_open_be_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_ce Z P C (open_be_rec k e2 e1) =
    open_be_rec k (subst_cb Z P C e2) (subst_ce Z P C e1)
with subst_cb_open_bb_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_cb Z P C (open_bb_rec k e2 e1) =
    open_bb_rec k (subst_cb Z P C e2) (subst_cb Z P C e1)
with subst_cs_open_bs_rec : ∀ e1 e2 Z P C k,
  block P →
  subst_cs Z P C (open_bs_rec k e2 e1) =
    open_bs_rec k (subst_cb Z P C e2) (subst_cs Z P C e1).

Lemma subst_ce_open_be : ∀ e1 e2 Z P C,
  block P →
  subst_ce Z P C (open_be e1 e2) = open_be (subst_ce Z P C e1) (subst_cb Z P C e2)
with subst_cb_open_bb : ∀ e1 e2 Z P C,
  block P →
  subst_cb Z P C (open_bb e1 e2) = open_bb (subst_cb Z P C e1) (subst_cb Z P C e2)
with subst_cs_open_bs : ∀ e1 e2 Z P C,
  block P →
  subst_cs Z P C (open_bs e1 e2) = open_bs (subst_cs Z P C e1) (subst_cb Z P C e2).

Lemma subst_ce_open_be_var : ∀ Z (x:atom) P C e,
  block P →
  x ≠ Z →
  open_be (subst_ce Z P C e) x = subst_ce Z P C (open_be e x)
with subst_cb_open_bb_var : ∀ Z (x:atom) P C e,
  block P →
  x ≠ Z →
  open_bb (subst_cb Z P C e) x = subst_cb Z P C (open_bb e x)
with subst_cs_open_bs_var : ∀ Z (x:atom) P C e,
  block P →
  x ≠ Z →
  open_bs (subst_cs Z P C e) x = subst_cs Z P C (open_bs e x).

Lemma subst_cvt_open_cvt_rec : ∀ T C1 C2 X k,
  capt C1 →
  subst_cvt X C1 (open_cvt_rec k C2 T) =
    open_cvt_rec k (subst_cset X C1 C2) (subst_cvt X C1 T)
with subst_cbt_open_cbt_rec : ∀ T C1 C2 X k,
  capt C1 →
  subst_cbt X C1 (open_cbt_rec k C2 T) =
    open_cbt_rec k (subst_cset X C1 C2) (subst_cbt X C1 T).

Lemma subst_cvt_open_cvt : ∀ T C1 C2 X,
  capt C1 →
  subst_cvt X C1 (open_cvt T C2) =
    open_cvt (subst_cvt X C1 T) (subst_cset X C1 C2)
with subst_cbt_open_cbt : ∀ T C1 C2 X,
  capt C1 →
  subst_cbt X C1 (open_cbt T C2) =
    open_cbt (subst_cbt X C1 T) (subst_cset X C1 C2).

Lemma subst_cvt_open_cvt_var : ∀ T C1 X (x:atom),
  x ≠ X →
  capt C1 →
  subst_cvt X C1 (open_cvt T (cset_fvar x)) =
    open_cvt (subst_cvt X C1 T) (cset_fvar x)
with subst_cbt_open_cbt_var : ∀ T C1 X (x:atom),
  x ≠ X →
  capt C1 →
  subst_cbt X C1 (open_cbt T (cset_fvar x)) =
    open_cbt (subst_cbt X C1 T) (cset_fvar x).

Lemma subst_ce_open_ce_rec : ∀ e1 e2 Z P C D k,
  block P →
  capt D →
  subst_ce Z P D (open_ce_rec k e2 C e1) =
    open_ce_rec k (subst_cb Z P D e2) (subst_cset Z D C) (subst_ce Z P D e1)
with subst_cb_open_cb_rec : ∀ e1 e2 Z P C D k,
  block P →
  capt D →
  subst_cb Z P D (open_cb_rec k e2 C e1) =
    open_cb_rec k (subst_cb Z P D e2) (subst_cset Z D C) (subst_cb Z P D e1)
with subst_cs_open_cs_rec : ∀ e1 e2 Z P C D k,
  block P →
  capt D →
  subst_cs Z P D (open_cs_rec k e2 C e1) =
    open_cs_rec k (subst_cb Z P D e2) (subst_cset Z D C) (subst_cs Z P D e1).

Lemma subst_ce_open_ce : ∀ e1 e2 Z P C D,
  block P →
  capt D →
  subst_ce Z P D (open_ce e1 e2 C) = open_ce (subst_ce Z P D e1) (subst_cb Z P D e2) (subst_cset Z D C)
with subst_cb_open_cb : ∀ e1 e2 Z P C D,
  block P →
  capt D →
  subst_cb Z P D (open_cb e1 e2 C) = open_cb (subst_cb Z P D e1) (subst_cb Z P D e2) (subst_cset Z D C)
with subst_cs_open_cs : ∀ e1 e2 Z P C D,
  block P →
  capt D →
  subst_cs Z P D (open_cs e1 e2 C) = open_cs (subst_cs Z P D e1) (subst_cb Z P D e2) (subst_cset Z D C).

Lemma subst_ce_open_ce_var : ∀ Z (x:atom) P e D,
  block P →
  capt D →
  x ≠ Z →
  open_ce (subst_ce Z P D e) x (cset_fvar x) = subst_ce Z P D (open_ce e x (cset_fvar x))
with subst_cb_open_cb_var : ∀ Z (x:atom) P e D,
  block P →
  capt D →
  x ≠ Z →
  open_cb (subst_cb Z P D e) x (cset_fvar x) = subst_cb Z P D (open_cb e x (cset_fvar x))
with subst_cs_open_cs_var : ∀ Z (x:atom) P e D,
  block P →
  capt D →
  x ≠ Z →
  open_cs (subst_cs Z P D e) x (cset_fvar x) = subst_cs Z P D (open_cs e x (cset_fvar x)).

Lemma subst_te_open_ee_rec : ∀ e1 e2 X U k,
  subst_te X U (open_ee_rec k e2 e1) =
    open_ee_rec k (subst_te X U e2) (subst_te X U e1)
with subst_tb_open_eb_rec : ∀ e1 e2 X U k,
  subst_tb X U (open_eb_rec k e2 e1) =
    open_eb_rec k (subst_te X U e2) (subst_tb X U e1)
with subst_ts_open_es_rec : ∀ e1 e2 X U k,
  subst_ts X U (open_es_rec k e2 e1) =
    open_es_rec k (subst_te X U e2) (subst_ts X U e1).

Lemma subst_te_open_ee : ∀ e1 e2 X U,
  subst_te X U (open_ee e1 e2) =
    open_ee (subst_te X U e1) (subst_te X U e2)
with subst_tb_open_eb : ∀ e1 e2 X U,
  subst_tb X U (open_eb e1 e2) =
    open_eb (subst_tb X U e1) (subst_te X U e2)
with subst_ts_open_es : ∀ e1 e2 X U,
  subst_ts X U (open_es e1 e2) =
    open_es (subst_ts X U e1) (subst_te X U e2).

Lemma subst_te_open_be_rec : ∀ e1 e2 X U k,
  subst_te X U (open_be_rec k e2 e1) =
    open_be_rec k (subst_tb X U e2) (subst_te X U e1)
with subst_tb_open_bb_rec : ∀ e1 e2 X U k,
  subst_tb X U (open_bb_rec k e2 e1) =
    open_bb_rec k (subst_tb X U e2) (subst_tb X U e1)
with subst_ts_open_bs_rec : ∀ e1 e2 X U k,
  subst_ts X U (open_bs_rec k e2 e1) =
    open_bs_rec k (subst_tb X U e2) (subst_ts X U e1).

Lemma subst_te_open_be : ∀ e1 e2 X U,
  subst_te X U (open_be e1 e2) =
    open_be (subst_te X U e1) (subst_tb X U e2)
with subst_tb_open_bb : ∀ e1 e2 X U,
  subst_tb X U (open_bb e1 e2) =
    open_bb (subst_tb X U e1) (subst_tb X U e2)
with subst_ts_open_bs : ∀ e1 e2 X U,
  subst_ts X U (open_bs e1 e2) =
    open_bs (subst_ts X U e1) (subst_tb X U e2).

Lemma subst_tvt_intro_rec : ∀ X T U k,
  X `notin` fv_tvt T →
  open_tvt_rec k U T = subst_tvt X U (open_tvt_rec k X T)
with subst_tbt_intro_rec : ∀ X T U k,
  X `notin` fv_tbt T →
  open_tbt_rec k U T = subst_tbt X U (open_tbt_rec k X T).

Lemma subst_te_intro_rec : ∀ X e T k,
  X `notin` fv_te e →
  open_te_rec k T e = subst_te X T (open_te_rec k X e)
with subst_ts_intro_rec : ∀ X e T k,
  X `notin` fv_ts e →
  open_ts_rec k T e = subst_ts X T (open_ts_rec k X e)
with subst_tb_intro_rec : ∀ X e T k,
  X `notin` fv_tb e →
  open_tb_rec k T e = subst_tb X T (open_tb_rec k X e).

Lemma subst_be_fresh : ∀ a s1 s2,
  a `notin` fv_be s2 →
  subst_be a s1 s2 = s2
with subst_bs_fresh : ∀ a s1 s2,
  a `notin` fv_bs s2 →
  subst_bs a s1 s2 = s2
with subst_bb_fresh : ∀ a s1 s2,
  a `notin` fv_bb s2 →
  subst_bb a s1 s2 = s2.

Lemma subst_ee_fresh : ∀ a s1 s2,
  a `notin` fv_ee s2 →
  subst_ee a s1 s2 = s2
with subst_es_fresh : ∀ a s1 s2,
  a `notin` fv_es s2 →
  subst_es a s1 s2 = s2
with subst_eb_fresh : ∀ a s1 s2,
  a `notin` fv_eb s2 →
  subst_eb a s1 s2 = s2.

Lemma subst_ee_through_subst_be : ∀ a1 a2 s1 s2 s,
  a1 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a2) →
  a2 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a1) →
  subst_be a1 s1 (subst_ee a2 s2 s) = subst_ee a2 s2 (subst_be a1 s1 s)
with subst_es_through_subst_bs : ∀ a1 a2 s1 s2 s,
  a1 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a2) →
  a2 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a1) →
  subst_bs a1 s1 (subst_es a2 s2 s) = subst_es a2 s2 (subst_bs a1 s1 s)
with subst_eb_through_subst_bb : ∀ a1 a2 s1 s2 s,
  a1 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a2) →
  a2 `notin` (fv_eb s1 `union` fv_bb s1 `union` fv_be s2 `union` singleton a1) →
  subst_bb a1 s1 (subst_eb a2 s2 s) = subst_eb a2 s2 (subst_bb a1 s1 s).

Lemma subst_tvt_intro : ∀ X T2 U,
  X `notin` fv_tvt T2 →
  open_tvt T2 U = subst_tvt X U (open_tvt T2 X)
with subst_tbt_intro : ∀ X T2 U,
  X `notin` fv_tbt T2 →
  open_tbt T2 U = subst_tbt X U (open_tbt T2 X).

Lemma open_tvt_rec_type_aux : ∀ T j V i U,
  i ≠ j →
  open_tvt_rec j V T = open_tvt_rec i U (open_tvt_rec j V T) →
  T = open_tvt_rec i U T
with open_tbt_rec_type_aux : ∀ T j V i U,
  i ≠ j →
  open_tbt_rec j V T = open_tbt_rec i U (open_tbt_rec j V T) →
  T = open_tbt_rec i U T.

Lemma open_tvt_rec_capt_aux : ∀ T j C i U,
  open_cvt_rec j C T = open_tvt_rec i U (open_cvt_rec j C T) →
  T = open_tvt_rec i U T
with open_tbt_rec_capt_aux : ∀ T j C i U,
  open_cbt_rec j C T = open_tbt_rec i U (open_cbt_rec j C T) →
  T = open_tbt_rec i U T.

Lemma open_tvt_rec_vtype : ∀ T U k,
  vtype T →
  T = open_tvt_rec k U T
with open_tbt_rec_btype : ∀ T U k,
  btype T →
  T = open_tbt_rec k U T.

Lemma subst_tvt_open_tvt_rec : ∀ T1 T2 X P k,
  vtype P →
  subst_tvt X P (open_tvt_rec k T2 T1) =
    open_tvt_rec k (subst_tvt X P T2) (subst_tvt X P T1)
with subst_tbt_open_tbt_rec : ∀ T1 T2 X P k,
  vtype P →
  subst_tbt X P (open_tbt_rec k T2 T1) =
    open_tbt_rec k (subst_tvt X P T2) (subst_tbt X P T1).

Lemma subst_tvt_open_tvt_var : ∀ (X Y:atom) P T,
  Y ≠ X →
  vtype P →
  open_tvt (subst_tvt X P T) Y = subst_tvt X P (open_tvt T Y)
with subst_tbt_open_tbt_var : ∀ (X Y:atom) P T,
  Y ≠ X →
  vtype P →
  open_tbt (subst_tbt X P T) Y = subst_tbt X P (open_tbt T Y).

Lemma subst_tvt_open_cvt_rec : ∀ T1 C X P k,
  vtype P →
  subst_tvt X P (open_cvt_rec k C T1) =
    open_cvt_rec k C (subst_tvt X P T1)
with subst_tbt_open_cbt_rec : ∀ T1 C X P k,
  vtype P →
  subst_tbt X P (open_cbt_rec k C T1) =
    open_cbt_rec k C (subst_tbt X P T1).

Lemma subst_tvt_open_cvt_var : ∀ (X Y:atom) P T,
  vtype P →
  open_cvt (subst_tvt X P T) (cset_fvar Y) =
    subst_tvt X P (open_cvt T (cset_fvar Y))
with subst_tbt_open_cbt_var : ∀ (X Y:atom) P T,
  vtype P →
  open_cbt (subst_tbt X P T) (cset_fvar Y) =
    subst_tbt X P (open_cbt T (cset_fvar Y)).

Lemma subst_cvt_fresh : ∀ X C T,
  X `notin` fv_cvt T →
  T = subst_cvt X C T
with subst_cbt_fresh : ∀ X C T,
  X `notin` fv_cbt T →
  T = subst_cbt X C T.

Lemma subst_cvt_open_tvt_rec : ∀ T C1 U X k,
  capt C1 →
  subst_cvt X C1 (open_tvt_rec k U T) =
    open_tvt_rec k (subst_cvt X C1 U) (subst_cvt X C1 T)
with subst_cbt_open_tbt_rec : ∀ T C1 U X k,
  capt C1 →
  subst_cbt X C1 (open_tbt_rec k U T) =
    open_tbt_rec k (subst_cvt X C1 U) (subst_cbt X C1 T).

Lemma subst_cvt_open_tvt : ∀ T C1 U X,
  capt C1 →
  subst_cvt X C1 (open_tvt T U) =
    open_tvt (subst_cvt X C1 T) (subst_cvt X C1 U)
with subst_cbt_open_tbt : ∀ T C1 U X,
  capt C1 →
  subst_cbt X C1 (open_tbt T U) =
    open_tbt (subst_cbt X C1 T) (subst_cvt X C1 U).

Lemma subst_cvt_open_tvt_var : ∀ T C1 X Y,
  Y ≠ X →
  capt C1 →
  subst_cvt X C1 (open_tvt T Y) =
    open_tvt (subst_cvt X C1 T) Y
with subst_cbt_open_tbt_var : ∀ T C1 X Y,
  Y ≠ X →
  capt C1 →
  subst_cbt X C1 (open_tbt T Y) =
    open_tbt (subst_cbt X C1 T) Y.

Lemma subst_tvt_open_cvt : ∀ T1 C X P,
  vtype P →
  subst_tvt X P (open_cvt T1 C) =
    open_cvt (subst_tvt X P T1) C
with subst_tbt_open_cbt : ∀ T1 C X P,
  vtype P →
  subst_tbt X P (open_cbt T1 C) =
    open_cbt (subst_tbt X P T1) C.

Lemma subst_te_open_ce_rec : ∀ e1 e2 C X U k,
  vtype U →
  subst_te X U (open_ce_rec k e2 C e1) =
    open_ce_rec k (subst_tb X U e2) C (subst_te X U e1)
with subst_tb_open_cb_rec : ∀ e1 e2 C X U k,
  vtype U →
  subst_tb X U (open_cb_rec k e2 C e1) =
    open_cb_rec k (subst_tb X U e2) C (subst_tb X U e1)
with subst_ts_open_cs_rec : ∀ e1 e2 C X U k,
  vtype U →
  subst_ts X U (open_cs_rec k e2 C e1) =
    open_cs_rec k (subst_tb X U e2) C (subst_ts X U e1).

Lemma subst_te_open_ce : ∀ e1 e2 C X U,
  vtype U →
  subst_te X U (open_ce e1 e2 C) =
    open_ce (subst_te X U e1) (subst_tb X U e2) C
with subst_tb_open_cb : ∀ e1 e2 C X U,
  vtype U →
  subst_tb X U (open_cb e1 e2 C) =
    open_cb (subst_tb X U e1) (subst_tb X U e2) C
with subst_ts_open_cs : ∀ e1 e2 C X U,
  vtype U →
  subst_ts X U (open_cs e1 e2 C) =
    open_cs (subst_ts X U e1) (subst_tb X U e2) C.

Lemma subst_tvt_open_tvt : ∀ T1 T2 X P,
  vtype P →
  subst_tvt X P (open_tvt T1 T2) =
    open_tvt (subst_tvt X P T1) (subst_tvt X P T2)
with subst_tbt_open_tbt : ∀ T1 T2 X P,
  vtype P →
  subst_tbt X P (open_tbt T1 T2) =
    open_tbt (subst_tbt X P T1) (subst_tvt X P T2).

Lemma subst_tvt_fresh : ∀ X U T,
  X `notin` fv_tvt T →
  T = subst_tvt X U T
with subst_tbt_fresh : ∀ X U T,
  X `notin` fv_tbt T →
  T = subst_tbt X U T.

Lemma subst_te_intro : ∀ x e u,
  x `notin` fv_te e →
  open_te e u = subst_te x u (open_te e x)
with subst_ts_intro : ∀ x e u,
  x `notin` fv_ts e →
  open_ts e u = subst_ts x u (open_ts e x)
with subst_tb_intro : ∀ x e u,
  x `notin` fv_tb e →
  open_tb e u = subst_tb x u (open_tb e x).

Lemma subst_te_open_te_rec : ∀ e1 W X U k,
  vtype U →
  subst_te X U (open_te_rec k W e1) =
    open_te_rec k (subst_tvt X U W) (subst_te X U e1)
with subst_tb_open_tb_rec : ∀ e1 W X U k,
  vtype U →
  subst_tb X U (open_tb_rec k W e1) =
    open_tb_rec k (subst_tvt X U W) (subst_tb X U e1)
with subst_ts_open_ts_rec : ∀ e1 W X U k,
  vtype U →
  subst_ts X U (open_ts_rec k W e1) =
    open_ts_rec k (subst_tvt X U W) (subst_ts X U e1).

Lemma subst_te_open_te : ∀ e1 W X U,
  vtype U →
  subst_te X U (open_te e1 W) =
    open_te (subst_te X U e1) (subst_tvt X U W)
with subst_tb_open_tb : ∀ e1 W X U,
  vtype U →
  subst_tb X U (open_tb e1 W) =
    open_tb (subst_tb X U e1) (subst_tvt X U W)
with subst_ts_open_ts : ∀ e1 W X U,
  vtype U →
  subst_ts X U (open_ts e1 W) =
    open_ts (subst_ts X U e1) (subst_tvt X U W).

Lemma open_te_rec_expr_aux : ∀ e j v T i,
  open_ee_rec j v e = open_te_rec i T (open_ee_rec j v e) →
  e = open_te_rec i T e
with open_tb_rec_expr_aux : ∀ e j v T i,
  open_eb_rec j v e = open_tb_rec i T (open_eb_rec j v e) →
  e = open_tb_rec i T e
with open_ts_rec_expr_aux : ∀ e j v T i,
  open_es_rec j v e = open_ts_rec i T (open_es_rec j v e) →
  e = open_ts_rec i T e.

Lemma open_te_rec_block_aux : ∀ e j v T i,
  open_be_rec j v e = open_te_rec i T (open_be_rec j v e) →
  e = open_te_rec i T e
with open_tb_rec_block_aux : ∀ e j v T i,
  open_bb_rec j v e = open_tb_rec i T (open_bb_rec j v e) →
  e = open_tb_rec i T e
with open_ts_rec_block_aux : ∀ e j v T i,
  open_bs_rec j v e = open_ts_rec i T (open_bs_rec j v e) →
  e = open_ts_rec i T e.

Lemma open_te_rec_capt_aux : ∀ e j C v T i,
  open_ce_rec j v C e = open_te_rec i T (open_ce_rec j v C e) →
  e = open_te_rec i T e
with open_tb_rec_capt_aux : ∀ e j C v T i,
  open_cb_rec j v C e = open_tb_rec i T (open_cb_rec j v C e) →
  e = open_tb_rec i T e
with open_ts_rec_capt_aux : ∀ e j C v T i,
  open_cs_rec j v C e = open_ts_rec i T (open_cs_rec j v C e) →
  e = open_ts_rec i T e.

Lemma open_te_rec_type_aux : ∀ e j U T i,
  i ≠ j →
  open_te_rec j U e = open_te_rec i T (open_te_rec j U e) →
  e = open_te_rec i T e
with open_tb_rec_type_aux : ∀ e j U T i,
  i ≠ j →
  open_tb_rec j U e = open_tb_rec i T (open_tb_rec j U e) →
  e = open_tb_rec i T e
with open_ts_rec_type_aux : ∀ e j U T i,
  i ≠ j →
  open_ts_rec j U e = open_ts_rec i T (open_ts_rec j U e) →
  e = open_ts_rec i T e.

Lemma open_te_rec_expr : ∀ k T e,
  expr e →
  e = open_te_rec k T e
with open_ts_rec_stmt : ∀ k T e,
  stmt e →
  e = open_ts_rec k T e
with open_tb_rec_block : ∀ k T e,
  block e →
  e = open_tb_rec k T e.

Lemma subst_ee_open_te_rec : ∀ e T x u k,
  expr u →
  subst_ee x u (open_te_rec k T e) =
    open_te_rec k T (subst_ee x u e)
with subst_eb_open_tb_rec : ∀ e T x u k,
  expr u →
  subst_eb x u (open_tb_rec k T e) =
    open_tb_rec k T (subst_eb x u e)
with subst_es_open_ts_rec : ∀ e T x u k,
  expr u →
  subst_es x u (open_ts_rec k T e) =
    open_ts_rec k T (subst_es x u e).

Lemma subst_ee_open_te: ∀ e T x u,
  expr u →
  subst_ee x u (open_te e T) =
    open_te (subst_ee x u e) T
with subst_eb_open_tb : ∀ e T x u,
  expr u →
  subst_eb x u (open_tb e T) =
    open_tb (subst_eb x u e) T
with subst_es_open_ts: ∀ e T x u,
  expr u →
  subst_es x u (open_ts e T) =
    open_ts (subst_es x u e) T.

Lemma subst_ee_open_te_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_te (subst_ee x u e) y = subst_ee x u (open_te e y)
with subst_eb_open_tb_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_tb (subst_eb x u e) y = subst_eb x u (open_tb e y)
with subst_es_open_ts_var : ∀ (x y:atom) u e,
  y ≠ x →
  expr u →
  open_ts (subst_es x u e) y = subst_es x u (open_ts e y).

Lemma subst_be_open_te_rec : ∀ e T x u k,
  block u →
  subst_be x u (open_te_rec k T e) =
    open_te_rec k T (subst_be x u e)
with subst_bb_open_tb_rec : ∀ e T x u k,
  block u →
  subst_bb x u (open_tb_rec k T e) =
    open_tb_rec k T (subst_bb x u e)
with subst_bs_open_ts_rec : ∀ e T x u k,
  block u →
  subst_bs x u (open_ts_rec k T e) =
    open_ts_rec k T (subst_bs x u e).

Lemma subst_be_open_te: ∀ e T x u,
  block u →
  subst_be x u (open_te e T) =
    open_te (subst_be x u e) T
with subst_bb_open_tb : ∀ e T x u,
  block u →
  subst_bb x u (open_tb e T) =
    open_tb (subst_bb x u e) T
with subst_bs_open_ts: ∀ e T x u,
  block u →
  subst_bs x u (open_ts e T) =
    open_ts (subst_bs x u e) T.

Lemma subst_be_open_te_var : ∀ (x y:atom) u e,
  y ≠ x →
  block u →
  open_te (subst_be x u e) y = subst_be x u (open_te e y)
with subst_bb_open_tb_var : ∀ (x y:atom) u e,
  y ≠ x →
  block u →
  open_tb (subst_bb x u e) y = subst_bb x u (open_tb e y)
with subst_bs_open_ts_var : ∀ (x y:atom) u e,
  y ≠ x →
  block u →
  open_ts (subst_bs x u e) y = subst_bs x u (open_ts e y).

Lemma subst_ce_open_te_rec : ∀ e T x u C k,
  capt C →
  block u →
  subst_ce x u C (open_te_rec k T e) =
    open_te_rec k (subst_cvt x C T) (subst_ce x u C e)
with subst_cb_open_tb_rec : ∀ e T x u C k,
  capt C →
  block u →
  subst_cb x u C (open_tb_rec k T e) =
    open_tb_rec k (subst_cvt x C T) (subst_cb x u C e)
with subst_cs_open_ts_rec : ∀ e T x u C k,
  capt C →
  block u →
  subst_cs x u C (open_ts_rec k T e) =
    open_ts_rec k (subst_cvt x C T) (subst_cs x u C e).

Lemma subst_ce_open_te: ∀ e T x u C,
  capt C →
  block u →
  subst_ce x u C (open_te e T) =
    open_te (subst_ce x u C e) (subst_cvt x C T)
with subst_cb_open_tb : ∀ e T x u C,
  capt C →
  block u →
  subst_cb x u C (open_tb e T) =
    open_tb (subst_cb x u C e) (subst_cvt x C T)
with subst_cs_open_ts: ∀ e T x u C,
  capt C →
  block u →
  subst_cs x u C (open_ts e T) =
    open_ts (subst_cs x u C e) (subst_cvt x C T).

Lemma subst_ce_open_te_var : ∀ (x y:atom) u e C,
  y ≠ x →
  capt C →
  block u →
  open_te (subst_ce x u C e) y = subst_ce x u C (open_te e y)
with subst_cb_open_tb_var : ∀ (x y:atom) u e C,
  y ≠ x →
  capt C →
  block u →
  open_tb (subst_cb x u C e) y = subst_cb x u C (open_tb e y)
with subst_cs_open_ts_var : ∀ (x y:atom) u e C,
  y ≠ x →
  capt C →
  block u →
  open_ts (subst_cs x u C e) y = subst_cs x u C (open_ts e y).