Infrastructure

Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.

Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.

Require Export Definitions.

NOTE: Auxiliary theorems are hidden in generated documentation. In general, there is a _rec version of every lemma involving open and close.

Induction principles for nonterminals


Scheme typ_ind' := Induction for typ Sort Prop
  with dtyp_ind' := Induction for dtyp Sort Prop.

Definition typ_dtyp_mutind :=
  fun H1 H2 H3 H4 H5 H6
  (conj (typ_ind' H1 H2 H3 H4 H5 H6)
  (dtyp_ind' H1 H2 H3 H4 H5 H6)).

Scheme typ_rec' := Induction for typ Sort Set
  with dtyp_rec' := Induction for dtyp Sort Set.

Definition typ_dtyp_mutrec :=
  fun H1 H2 H3 H4 H5 H6
  (pair (typ_rec' H1 H2 H3 H4 H5 H6)
  (dtyp_rec' H1 H2 H3 H4 H5 H6)).

Scheme label_ind' := Induction for label Sort Prop.

Definition label_mutind :=
  fun H1 H2 H3
  label_ind' H1 H2 H3.

Scheme label_rec' := Induction for label Sort Set.

Definition label_mutrec :=
  fun H1 H2 H3
  label_rec' H1 H2 H3.

Scheme trm_ind' := Induction for trm Sort Prop.

Definition trm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12
  trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.

Scheme trm_rec' := Induction for trm Sort Set.

Definition trm_mutrec :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12
  trm_rec' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.

Scheme ityp_ind' := Induction for ityp Sort Prop.

Definition ityp_mutind :=
  fun H1 H2 H3
  ityp_ind' H1 H2 H3.

Scheme ityp_rec' := Induction for ityp Sort Set.

Definition ityp_mutrec :=
  fun H1 H2 H3
  ityp_rec' H1 H2 H3.

Scheme itrm_ind' := Induction for itrm Sort Prop.

Definition itrm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8
  itrm_ind' H1 H2 H3 H4 H5 H6 H7 H8.

Scheme itrm_rec' := Induction for itrm Sort Set.

Definition itrm_mutrec :=
  fun H1 H2 H3 H4 H5 H6 H7 H8
  itrm_rec' H1 H2 H3 H4 H5 H6 H7 H8.

Close


Fixpoint close_trm_wrt_trm_rec (n1 : nat) (x1 : var) (L1 : trm) {struct L1} : trm :=
  match L1 with
    | t_var_f x2if (x1 == x2) then (t_var_b n1) else (t_var_f x2)
    | t_var_b n2if (lt_ge_dec n2 n1) then (t_var_b n2) else (t_var_b (S n2))
    | t_const c1t_const c1
    | t_binop M1 N1t_binop (close_trm_wrt_trm_rec n1 x1 M1) (close_trm_wrt_trm_rec n1 x1 N1)
    | t_abs A1 N1t_abs A1 (close_trm_wrt_trm_rec (S n1) x1 N1)
    | t_app L2 M1t_app (close_trm_wrt_trm_rec n1 x1 L2) (close_trm_wrt_trm_rec n1 x1 M1)
    | t_nullt_null
    | t_lift M1t_lift (close_trm_wrt_trm_rec n1 x1 M1)
    | t_case L2 M1 N1t_case (close_trm_wrt_trm_rec n1 x1 L2) (close_trm_wrt_trm_rec n1 x1 M1) (close_trm_wrt_trm_rec (S n1) x1 N1)
    | t_cast M1 A1 p1 B1t_cast (close_trm_wrt_trm_rec n1 x1 M1) A1 p1 B1
    | t_blame p1t_blame p1
  end.

Definition close_trm_wrt_trm x1 L1 := close_trm_wrt_trm_rec 0 x1 L1.

Fixpoint close_itrm_wrt_itrm_rec (n1 : nat) (ix1 : ivar) (iL1 : itrm) {struct iL1} : itrm :=
  match iL1 with
    | itrm_var_f ix2if (ix1 == ix2) then (itrm_var_b n1) else (itrm_var_f ix2)
    | itrm_var_b n2if (lt_ge_dec n2 n1) then (itrm_var_b n2) else (itrm_var_b (S n2))
    | itrm_const c1itrm_const c1
    | itrm_binop iM1 iN1itrm_binop (close_itrm_wrt_itrm_rec n1 ix1 iM1) (close_itrm_wrt_itrm_rec n1 ix1 iN1)
    | itrm_abs iA1 iN1itrm_abs iA1 (close_itrm_wrt_itrm_rec (S n1) ix1 iN1)
    | itrm_app iL2 iM1itrm_app (close_itrm_wrt_itrm_rec n1 ix1 iL2) (close_itrm_wrt_itrm_rec n1 ix1 iM1)
    | itrm_nullitrm_null
  end.

Definition close_itrm_wrt_itrm ix1 iL1 := close_itrm_wrt_itrm_rec 0 ix1 iL1.

Size


Fixpoint size_typ (A1 : typ) {struct A1} : nat :=
  match A1 with
    | typ_def D1 ⇒ 1 + (size_dtyp D1)
    | typ_null D1 ⇒ 1 + (size_dtyp D1)
  end

with size_dtyp (D1 : dtyp) {struct D1} : nat :=
  match D1 with
    | dtyp_base ⇒ 1
    | dtyp_arrow A1 B1 ⇒ 1 + (size_typ A1) + (size_typ B1)
  end.

Fixpoint size_label (p1 : label) {struct p1} : nat :=
  match p1 with
    | label_name bl1 ⇒ 1
    | label_not_label bl1 ⇒ 1
  end.

Fixpoint size_trm (L1 : trm) {struct L1} : nat :=
  match L1 with
    | t_var_f x1 ⇒ 1
    | t_var_b n1 ⇒ 1
    | t_const c1 ⇒ 1
    | t_binop M1 N1 ⇒ 1 + (size_trm M1) + (size_trm N1)
    | t_abs A1 N1 ⇒ 1 + (size_typ A1) + (size_trm N1)
    | t_app L2 M1 ⇒ 1 + (size_trm L2) + (size_trm M1)
    | t_null ⇒ 1
    | t_lift M1 ⇒ 1 + (size_trm M1)
    | t_case L2 M1 N1 ⇒ 1 + (size_trm L2) + (size_trm M1) + (size_trm N1)
    | t_cast M1 A1 p1 B1 ⇒ 1 + (size_trm M1) + (size_typ A1) + (size_label p1) + (size_typ B1)
    | t_blame p1 ⇒ 1 + (size_label p1)
  end.

Fixpoint size_ityp (iA1 : ityp) {struct iA1} : nat :=
  match iA1 with
    | ityp_base ⇒ 1
    | ityp_arrow iA2 iB1 ⇒ 1 + (size_ityp iA2) + (size_ityp iB1)
  end.

Fixpoint size_itrm (iL1 : itrm) {struct iL1} : nat :=
  match iL1 with
    | itrm_var_f ix1 ⇒ 1
    | itrm_var_b n1 ⇒ 1
    | itrm_const c1 ⇒ 1
    | itrm_binop iM1 iN1 ⇒ 1 + (size_itrm iM1) + (size_itrm iN1)
    | itrm_abs iA1 iN1 ⇒ 1 + (size_ityp iA1) + (size_itrm iN1)
    | itrm_app iL2 iM1 ⇒ 1 + (size_itrm iL2) + (size_itrm iM1)
    | itrm_null ⇒ 1
  end.

Degree

These define only an upper bound, not a strict upper bound.

Inductive degree_trm_wrt_trm : nat trm Prop :=
  | degree_wrt_trm_t_var_f : n1 x1,
    degree_trm_wrt_trm n1 (t_var_f x1)
  | degree_wrt_trm_t_var_b : n1 n2,
    lt n2 n1
    degree_trm_wrt_trm n1 (t_var_b n2)
  | degree_wrt_trm_t_const : n1 c1,
    degree_trm_wrt_trm n1 (t_const c1)
  | degree_wrt_trm_t_binop : n1 M1 N1,
    degree_trm_wrt_trm n1 M1
    degree_trm_wrt_trm n1 N1
    degree_trm_wrt_trm n1 (t_binop M1 N1)
  | degree_wrt_trm_t_abs : n1 A1 N1,
    degree_trm_wrt_trm (S n1) N1
    degree_trm_wrt_trm n1 (t_abs A1 N1)
  | degree_wrt_trm_t_app : n1 L1 M1,
    degree_trm_wrt_trm n1 L1
    degree_trm_wrt_trm n1 M1
    degree_trm_wrt_trm n1 (t_app L1 M1)
  | degree_wrt_trm_t_null : n1,
    degree_trm_wrt_trm n1 (t_null)
  | degree_wrt_trm_t_lift : n1 M1,
    degree_trm_wrt_trm n1 M1
    degree_trm_wrt_trm n1 (t_lift M1)
  | degree_wrt_trm_t_case : n1 L1 M1 N1,
    degree_trm_wrt_trm n1 L1
    degree_trm_wrt_trm n1 M1
    degree_trm_wrt_trm (S n1) N1
    degree_trm_wrt_trm n1 (t_case L1 M1 N1)
  | degree_wrt_trm_t_cast : n1 M1 A1 p1 B1,
    degree_trm_wrt_trm n1 M1
    degree_trm_wrt_trm n1 (t_cast M1 A1 p1 B1)
  | degree_wrt_trm_t_blame : n1 p1,
    degree_trm_wrt_trm n1 (t_blame p1).

Scheme degree_trm_wrt_trm_ind' := Induction for degree_trm_wrt_trm Sort Prop.

Definition degree_trm_wrt_trm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12
  degree_trm_wrt_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.

Hint Constructors degree_trm_wrt_trm : core lngen.

Inductive degree_itrm_wrt_itrm : nat itrm Prop :=
  | degree_wrt_itrm_itrm_var_f : n1 ix1,
    degree_itrm_wrt_itrm n1 (itrm_var_f ix1)
  | degree_wrt_itrm_itrm_var_b : n1 n2,
    lt n2 n1
    degree_itrm_wrt_itrm n1 (itrm_var_b n2)
  | degree_wrt_itrm_itrm_const : n1 c1,
    degree_itrm_wrt_itrm n1 (itrm_const c1)
  | degree_wrt_itrm_itrm_binop : n1 iM1 iN1,
    degree_itrm_wrt_itrm n1 iM1
    degree_itrm_wrt_itrm n1 iN1
    degree_itrm_wrt_itrm n1 (itrm_binop iM1 iN1)
  | degree_wrt_itrm_itrm_abs : n1 iA1 iN1,
    degree_itrm_wrt_itrm (S n1) iN1
    degree_itrm_wrt_itrm n1 (itrm_abs iA1 iN1)
  | degree_wrt_itrm_itrm_app : n1 iL1 iM1,
    degree_itrm_wrt_itrm n1 iL1
    degree_itrm_wrt_itrm n1 iM1
    degree_itrm_wrt_itrm n1 (itrm_app iL1 iM1)
  | degree_wrt_itrm_itrm_null : n1,
    degree_itrm_wrt_itrm n1 (itrm_null).

Scheme degree_itrm_wrt_itrm_ind' := Induction for degree_itrm_wrt_itrm Sort Prop.

Definition degree_itrm_wrt_itrm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8
  degree_itrm_wrt_itrm_ind' H1 H2 H3 H4 H5 H6 H7 H8.

Hint Constructors degree_itrm_wrt_itrm : core lngen.

Local closure (version in Set, induction principles)


Inductive lc_set_trm : trm Set :=
  | lc_set_t_var_f : x1,
    lc_set_trm (t_var_f x1)
  | lc_set_t_const : c1,
    lc_set_trm (t_const c1)
  | lc_set_t_binop : M1 N1,
    lc_set_trm M1
    lc_set_trm N1
    lc_set_trm (t_binop M1 N1)
  | lc_set_t_abs : A1 N1,
    ( x1 : var, lc_set_trm (open_trm_wrt_trm N1 (t_var_f x1)))
    lc_set_trm (t_abs A1 N1)
  | lc_set_t_app : L1 M1,
    lc_set_trm L1
    lc_set_trm M1
    lc_set_trm (t_app L1 M1)
  | lc_set_t_null :
    lc_set_trm (t_null)
  | lc_set_t_lift : M1,
    lc_set_trm M1
    lc_set_trm (t_lift M1)
  | lc_set_t_case : L1 M1 N1,
    lc_set_trm L1
    lc_set_trm M1
    ( x1 : var, lc_set_trm (open_trm_wrt_trm N1 (t_var_f x1)))
    lc_set_trm (t_case L1 M1 N1)
  | lc_set_t_cast : M1 A1 p1 B1,
    lc_set_trm M1
    lc_set_trm (t_cast M1 A1 p1 B1)
  | lc_set_t_blame : p1,
    lc_set_trm (t_blame p1).

Scheme lc_trm_ind' := Induction for lc_trm Sort Prop.

Definition lc_trm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11
  lc_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.

Scheme lc_set_trm_ind' := Induction for lc_set_trm Sort Prop.

Definition lc_set_trm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11
  lc_set_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.

Scheme lc_set_trm_rec' := Induction for lc_set_trm Sort Set.

Definition lc_set_trm_mutrec :=
  fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11
  lc_set_trm_rec' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.

Hint Constructors lc_trm : core lngen.

Hint Constructors lc_set_trm : core lngen.

Inductive lc_set_itrm : itrm Set :=
  | lc_set_itrm_var_f : ix1,
    lc_set_itrm (itrm_var_f ix1)
  | lc_set_itrm_const : c1,
    lc_set_itrm (itrm_const c1)
  | lc_set_itrm_binop : iM1 iN1,
    lc_set_itrm iM1
    lc_set_itrm iN1
    lc_set_itrm (itrm_binop iM1 iN1)
  | lc_set_itrm_abs : iA1 iN1,
    ( ix1 : ivar, lc_set_itrm (open_itrm_wrt_itrm iN1 (itrm_var_f ix1)))
    lc_set_itrm (itrm_abs iA1 iN1)
  | lc_set_itrm_app : iL1 iM1,
    lc_set_itrm iL1
    lc_set_itrm iM1
    lc_set_itrm (itrm_app iL1 iM1)
  | lc_set_itrm_null :
    lc_set_itrm (itrm_null).

Scheme lc_itrm_ind' := Induction for lc_itrm Sort Prop.

Definition lc_itrm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7
  lc_itrm_ind' H1 H2 H3 H4 H5 H6 H7.

Scheme lc_set_itrm_ind' := Induction for lc_set_itrm Sort Prop.

Definition lc_set_itrm_mutind :=
  fun H1 H2 H3 H4 H5 H6 H7
  lc_set_itrm_ind' H1 H2 H3 H4 H5 H6 H7.

Scheme lc_set_itrm_rec' := Induction for lc_set_itrm Sort Set.

Definition lc_set_itrm_mutrec :=
  fun H1 H2 H3 H4 H5 H6 H7
  lc_set_itrm_rec' H1 H2 H3 H4 H5 H6 H7.

Hint Constructors lc_itrm : core lngen.

Hint Constructors lc_set_itrm : core lngen.

Body


Definition body_trm_wrt_trm L1 := x1, lc_trm (open_trm_wrt_trm L1 (t_var_f x1)).

Hint Unfold body_trm_wrt_trm : core.

Definition body_itrm_wrt_itrm iL1 := ix1, lc_itrm (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)).

Hint Unfold body_itrm_wrt_itrm : core.

Tactic support

Additional hint declarations.

Hint Resolve @plus_le_compat : lngen.

Redefine some tactics.

Ltac default_case_split ::=
  first
    [ progress destruct_notin
    | progress destruct_sum
    | progress safe_f_equal
    ].

Theorems about size


Ltac default_auto ::= auto with arith lngen; tauto.
Ltac default_autorewrite ::= fail.


Lemma size_typ_min :
A1, 1 size_typ A1.
Proof.
pose proof size_typ_min_size_dtyp_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_typ_min : lngen.

Lemma size_dtyp_min :
D1, 1 size_dtyp D1.
Proof.
pose proof size_typ_min_size_dtyp_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_dtyp_min : lngen.


Lemma size_label_min :
p1, 1 size_label p1.
Proof.
pose proof size_label_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_label_min : lngen.


Lemma size_trm_min :
L1, 1 size_trm L1.
Proof.
pose proof size_trm_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_trm_min : lngen.


Lemma size_ityp_min :
iA1, 1 size_ityp iA1.
Proof.
pose proof size_ityp_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_ityp_min : lngen.


Lemma size_itrm_min :
iL1, 1 size_itrm iL1.
Proof.
pose proof size_itrm_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_itrm_min : lngen.





Lemma size_trm_close_trm_wrt_trm :
L1 x1,
  size_trm (close_trm_wrt_trm x1 L1) = size_trm L1.
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.

Hint Resolve size_trm_close_trm_wrt_trm : lngen.
Hint Rewrite size_trm_close_trm_wrt_trm using solve [auto] : lngen.

Lemma size_itrm_close_itrm_wrt_itrm :
iL1 ix1,
  size_itrm (close_itrm_wrt_itrm ix1 iL1) = size_itrm iL1.
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve size_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite size_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.





Lemma size_trm_open_trm_wrt_trm :
L1 L2,
  size_trm L1 size_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve size_trm_open_trm_wrt_trm : lngen.

Lemma size_itrm_open_itrm_wrt_itrm :
iL1 iL2,
  size_itrm iL1 size_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve size_itrm_open_itrm_wrt_itrm : lngen.





Lemma size_trm_open_trm_wrt_trm_var :
L1 x1,
  size_trm (open_trm_wrt_trm L1 (t_var_f x1)) = size_trm L1.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve size_trm_open_trm_wrt_trm_var : lngen.
Hint Rewrite size_trm_open_trm_wrt_trm_var using solve [auto] : lngen.

Lemma size_itrm_open_itrm_wrt_itrm_var :
iL1 ix1,
  size_itrm (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)) = size_itrm iL1.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve size_itrm_open_itrm_wrt_itrm_var : lngen.
Hint Rewrite size_itrm_open_itrm_wrt_itrm_var using solve [auto] : lngen.

Theorems about degree


Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.


Lemma degree_trm_wrt_trm_S :
n1 L1,
  degree_trm_wrt_trm n1 L1
  degree_trm_wrt_trm (S n1) L1.
Proof.
pose proof degree_trm_wrt_trm_S_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_trm_wrt_trm_S : lngen.


Lemma degree_itrm_wrt_itrm_S :
n1 iL1,
  degree_itrm_wrt_itrm n1 iL1
  degree_itrm_wrt_itrm (S n1) iL1.
Proof.
pose proof degree_itrm_wrt_itrm_S_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_itrm_wrt_itrm_S : lngen.

Lemma degree_trm_wrt_trm_O :
n1 L1,
  degree_trm_wrt_trm O L1
  degree_trm_wrt_trm n1 L1.
Proof.
induction n1; default_simp.
Qed.

Hint Resolve degree_trm_wrt_trm_O : lngen.

Lemma degree_itrm_wrt_itrm_O :
n1 iL1,
  degree_itrm_wrt_itrm O iL1
  degree_itrm_wrt_itrm n1 iL1.
Proof.
induction n1; default_simp.
Qed.

Hint Resolve degree_itrm_wrt_itrm_O : lngen.





Lemma degree_trm_wrt_trm_close_trm_wrt_trm :
L1 x1,
  degree_trm_wrt_trm 0 L1
  degree_trm_wrt_trm 1 (close_trm_wrt_trm x1 L1).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.

Hint Resolve degree_trm_wrt_trm_close_trm_wrt_trm : lngen.

Lemma degree_itrm_wrt_itrm_close_itrm_wrt_itrm :
iL1 ix1,
  degree_itrm_wrt_itrm 0 iL1
  degree_itrm_wrt_itrm 1 (close_itrm_wrt_itrm ix1 iL1).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve degree_itrm_wrt_itrm_close_itrm_wrt_itrm : lngen.





Lemma degree_trm_wrt_trm_close_trm_wrt_trm_inv :
L1 x1,
  degree_trm_wrt_trm 1 (close_trm_wrt_trm x1 L1)
  degree_trm_wrt_trm 0 L1.
Proof.
unfold close_trm_wrt_trm; eauto with lngen.
Qed.

Hint Immediate degree_trm_wrt_trm_close_trm_wrt_trm_inv : lngen.

Lemma degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv :
iL1 ix1,
  degree_itrm_wrt_itrm 1 (close_itrm_wrt_itrm ix1 iL1)
  degree_itrm_wrt_itrm 0 iL1.
Proof.
unfold close_itrm_wrt_itrm; eauto with lngen.
Qed.

Hint Immediate degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv : lngen.





Lemma degree_trm_wrt_trm_open_trm_wrt_trm :
L1 L2,
  degree_trm_wrt_trm 1 L1
  degree_trm_wrt_trm 0 L2
  degree_trm_wrt_trm 0 (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve degree_trm_wrt_trm_open_trm_wrt_trm : lngen.

Lemma degree_itrm_wrt_itrm_open_itrm_wrt_itrm :
iL1 iL2,
  degree_itrm_wrt_itrm 1 iL1
  degree_itrm_wrt_itrm 0 iL2
  degree_itrm_wrt_itrm 0 (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve degree_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.





Lemma degree_trm_wrt_trm_open_trm_wrt_trm_inv :
L1 L2,
  degree_trm_wrt_trm 0 (open_trm_wrt_trm L1 L2)
  degree_trm_wrt_trm 1 L1.
Proof.
unfold open_trm_wrt_trm; eauto with lngen.
Qed.

Hint Immediate degree_trm_wrt_trm_open_trm_wrt_trm_inv : lngen.

Lemma degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv :
iL1 iL2,
  degree_itrm_wrt_itrm 0 (open_itrm_wrt_itrm iL1 iL2)
  degree_itrm_wrt_itrm 1 iL1.
Proof.
unfold open_itrm_wrt_itrm; eauto with lngen.
Qed.

Hint Immediate degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv : lngen.

Theorems about open and close


Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= fail.





Lemma close_trm_wrt_trm_inj :
L1 L2 x1,
  close_trm_wrt_trm x1 L1 = close_trm_wrt_trm x1 L2
  L1 = L2.
Proof.
unfold close_trm_wrt_trm; eauto with lngen.
Qed.

Hint Immediate close_trm_wrt_trm_inj : lngen.

Lemma close_itrm_wrt_itrm_inj :
iL1 iL2 ix1,
  close_itrm_wrt_itrm ix1 iL1 = close_itrm_wrt_itrm ix1 iL2
  iL1 = iL2.
Proof.
unfold close_itrm_wrt_itrm; eauto with lngen.
Qed.

Hint Immediate close_itrm_wrt_itrm_inj : lngen.





Lemma close_trm_wrt_trm_open_trm_wrt_trm :
L1 x1,
  x1 `notin` fv_trm L1
  close_trm_wrt_trm x1 (open_trm_wrt_trm L1 (t_var_f x1)) = L1.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve close_trm_wrt_trm_open_trm_wrt_trm : lngen.
Hint Rewrite close_trm_wrt_trm_open_trm_wrt_trm using solve [auto] : lngen.

Lemma close_itrm_wrt_itrm_open_itrm_wrt_itrm :
iL1 ix1,
  ix1 `notin` fv_itrm iL1
  close_itrm_wrt_itrm ix1 (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)) = iL1.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve close_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.
Hint Rewrite close_itrm_wrt_itrm_open_itrm_wrt_itrm using solve [auto] : lngen.





Lemma open_trm_wrt_trm_close_trm_wrt_trm :
L1 x1,
  open_trm_wrt_trm (close_trm_wrt_trm x1 L1) (t_var_f x1) = L1.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve open_trm_wrt_trm_close_trm_wrt_trm : lngen.
Hint Rewrite open_trm_wrt_trm_close_trm_wrt_trm using solve [auto] : lngen.

Lemma open_itrm_wrt_itrm_close_itrm_wrt_itrm :
iL1 ix1,
  open_itrm_wrt_itrm (close_itrm_wrt_itrm ix1 iL1) (itrm_var_f ix1) = iL1.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve open_itrm_wrt_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite open_itrm_wrt_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.





Lemma open_trm_wrt_trm_inj :
L2 L1 x1,
  x1 `notin` fv_trm L2
  x1 `notin` fv_trm L1
  open_trm_wrt_trm L2 (t_var_f x1) = open_trm_wrt_trm L1 (t_var_f x1)
  L2 = L1.
Proof.
unfold open_trm_wrt_trm; eauto with lngen.
Qed.

Hint Immediate open_trm_wrt_trm_inj : lngen.

Lemma open_itrm_wrt_itrm_inj :
iL2 iL1 ix1,
  ix1 `notin` fv_itrm iL2
  ix1 `notin` fv_itrm iL1
  open_itrm_wrt_itrm iL2 (itrm_var_f ix1) = open_itrm_wrt_itrm iL1 (itrm_var_f ix1)
  iL2 = iL1.
Proof.
unfold open_itrm_wrt_itrm; eauto with lngen.
Qed.

Hint Immediate open_itrm_wrt_itrm_inj : lngen.

Theorems about lc


Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.


Lemma degree_trm_wrt_trm_of_lc_trm :
L1,
  lc_trm L1
  degree_trm_wrt_trm 0 L1.
Proof.
pose proof degree_trm_wrt_trm_of_lc_trm_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_trm_wrt_trm_of_lc_trm : lngen.


Lemma degree_itrm_wrt_itrm_of_lc_itrm :
iL1,
  lc_itrm iL1
  degree_itrm_wrt_itrm 0 iL1.
Proof.
pose proof degree_itrm_wrt_itrm_of_lc_itrm_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_itrm_wrt_itrm_of_lc_itrm : lngen.


Lemma lc_trm_of_degree :
L1,
  degree_trm_wrt_trm 0 L1
  lc_trm L1.
Proof.
intros L1; intros;
pose proof (lc_trm_of_degree_size_mutual (size_trm L1));
intuition eauto.
Qed.

Hint Resolve lc_trm_of_degree : lngen.


Lemma lc_itrm_of_degree :
iL1,
  degree_itrm_wrt_itrm 0 iL1
  lc_itrm iL1.
Proof.
intros iL1; intros;
pose proof (lc_itrm_of_degree_size_mutual (size_itrm iL1));
intuition eauto.
Qed.

Hint Resolve lc_itrm_of_degree : lngen.

Ltac typ_dtyp_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _
              fail 1
            | H : _ |- _
              fail 1
          end).

Ltac label_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _
              fail 1
          end).

Ltac trm_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _
              let J1 := fresh in pose proof H as J1; apply degree_trm_wrt_trm_of_lc_trm in J1; clear H
          end).

Ltac ityp_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _
              fail 1
          end).

Ltac itrm_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _
              let J1 := fresh in pose proof H as J1; apply degree_itrm_wrt_itrm_of_lc_itrm in J1; clear H
          end).

Lemma lc_t_abs_exists :
x1 A1 N1,
  lc_trm (open_trm_wrt_trm N1 (t_var_f x1))
  lc_trm (t_abs A1 N1).
Proof.
intros; trm_lc_exists_tac; eauto with lngen.
Qed.

Lemma lc_t_case_exists :
x1 L1 M1 N1,
  lc_trm L1
  lc_trm M1
  lc_trm (open_trm_wrt_trm N1 (t_var_f x1))
  lc_trm (t_case L1 M1 N1).
Proof.
intros; trm_lc_exists_tac; eauto with lngen.
Qed.

Lemma lc_itrm_abs_exists :
ix1 iA1 iN1,
  lc_itrm (open_itrm_wrt_itrm iN1 (itrm_var_f ix1))
  lc_itrm (itrm_abs iA1 iN1).
Proof.
intros; itrm_lc_exists_tac; eauto with lngen.
Qed.

Hint Extern 1 (lc_trm (t_abs _ _)) ⇒
  let x1 := fresh in
  pick_fresh x1;
  apply (lc_t_abs_exists x1) : core.

Hint Extern 1 (lc_trm (t_case _ _ _)) ⇒
  let x1 := fresh in
  pick_fresh x1;
  apply (lc_t_case_exists x1) : core.

Hint Extern 1 (lc_itrm (itrm_abs _ _)) ⇒
  let ix1 := fresh in
  pick_fresh ix1;
  apply (lc_itrm_abs_exists ix1) : core.

Lemma lc_body_trm_wrt_trm :
L1 L2,
  body_trm_wrt_trm L1
  lc_trm L2
  lc_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold body_trm_wrt_trm;
default_simp;
let x1 := fresh "x" in
pick_fresh x1;
specialize_all x1;
trm_lc_exists_tac;
eauto with lngen.
Qed.

Hint Resolve lc_body_trm_wrt_trm : lngen.

Lemma lc_body_itrm_wrt_itrm :
iL1 iL2,
  body_itrm_wrt_itrm iL1
  lc_itrm iL2
  lc_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold body_itrm_wrt_itrm;
default_simp;
let ix1 := fresh "x" in
pick_fresh ix1;
specialize_all ix1;
itrm_lc_exists_tac;
eauto with lngen.
Qed.

Hint Resolve lc_body_itrm_wrt_itrm : lngen.

Lemma lc_body_t_abs_2 :
A1 N1,
  lc_trm (t_abs A1 N1)
  body_trm_wrt_trm N1.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_t_abs_2 : lngen.

Lemma lc_body_t_case_3 :
L1 M1 N1,
  lc_trm (t_case L1 M1 N1)
  body_trm_wrt_trm N1.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_t_case_3 : lngen.

Lemma lc_body_itrm_abs_2 :
iA1 iN1,
  lc_itrm (itrm_abs iA1 iN1)
  body_itrm_wrt_itrm iN1.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_itrm_abs_2 : lngen.


Lemma lc_trm_unique :
L1 (proof2 proof3 : lc_trm L1), proof2 = proof3.
Proof.
pose proof lc_trm_unique_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_trm_unique : lngen.


Lemma lc_itrm_unique :
iL1 (proof2 proof3 : lc_itrm iL1), proof2 = proof3.
Proof.
pose proof lc_itrm_unique_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_itrm_unique : lngen.


Lemma lc_trm_of_lc_set_trm :
L1, lc_set_trm L1 lc_trm L1.
Proof.
pose proof lc_trm_of_lc_set_trm_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_trm_of_lc_set_trm : lngen.


Lemma lc_itrm_of_lc_set_itrm :
iL1, lc_set_itrm iL1 lc_itrm iL1.
Proof.
pose proof lc_itrm_of_lc_set_itrm_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_itrm_of_lc_set_itrm : lngen.


Lemma lc_set_trm_of_lc_trm :
L1,
  lc_trm L1
  lc_set_trm L1.
Proof.
intros L1; intros;
pose proof (lc_set_trm_of_lc_trm_size_mutual (size_trm L1));
intuition eauto.
Qed.

Hint Resolve lc_set_trm_of_lc_trm : lngen.


Lemma lc_set_itrm_of_lc_itrm :
iL1,
  lc_itrm iL1
  lc_set_itrm iL1.
Proof.
intros iL1; intros;
pose proof (lc_set_itrm_of_lc_itrm_size_mutual (size_itrm iL1));
intuition eauto.
Qed.

Hint Resolve lc_set_itrm_of_lc_itrm : lngen.

More theorems about open and close


Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.





Lemma close_trm_wrt_trm_lc_trm :
L1 x1,
  lc_trm L1
  x1 `notin` fv_trm L1
  close_trm_wrt_trm x1 L1 = L1.
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.

Hint Resolve close_trm_wrt_trm_lc_trm : lngen.
Hint Rewrite close_trm_wrt_trm_lc_trm using solve [auto] : lngen.

Lemma close_itrm_wrt_itrm_lc_itrm :
iL1 ix1,
  lc_itrm iL1
  ix1 `notin` fv_itrm iL1
  close_itrm_wrt_itrm ix1 iL1 = iL1.
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve close_itrm_wrt_itrm_lc_itrm : lngen.
Hint Rewrite close_itrm_wrt_itrm_lc_itrm using solve [auto] : lngen.





Lemma open_trm_wrt_trm_lc_trm :
L2 L1,
  lc_trm L2
  open_trm_wrt_trm L2 L1 = L2.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve open_trm_wrt_trm_lc_trm : lngen.
Hint Rewrite open_trm_wrt_trm_lc_trm using solve [auto] : lngen.

Lemma open_itrm_wrt_itrm_lc_itrm :
iL2 iL1,
  lc_itrm iL2
  open_itrm_wrt_itrm iL2 iL1 = iL2.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve open_itrm_wrt_itrm_lc_itrm : lngen.
Hint Rewrite open_itrm_wrt_itrm_lc_itrm using solve [auto] : lngen.

Theorems about fv


Ltac default_auto ::= auto with set lngen; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.





Lemma fv_trm_close_trm_wrt_trm :
L1 x1,
  fv_trm (close_trm_wrt_trm x1 L1) [=] remove x1 (fv_trm L1).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.

Hint Resolve fv_trm_close_trm_wrt_trm : lngen.
Hint Rewrite fv_trm_close_trm_wrt_trm using solve [auto] : lngen.

Lemma fv_itrm_close_itrm_wrt_itrm :
iL1 ix1,
  fv_itrm (close_itrm_wrt_itrm ix1 iL1) [=] remove ix1 (fv_itrm iL1).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve fv_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite fv_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.





Lemma fv_trm_open_trm_wrt_trm_lower :
L1 L2,
  fv_trm L1 [<=] fv_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve fv_trm_open_trm_wrt_trm_lower : lngen.

Lemma fv_itrm_open_itrm_wrt_itrm_lower :
iL1 iL2,
  fv_itrm iL1 [<=] fv_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve fv_itrm_open_itrm_wrt_itrm_lower : lngen.





Lemma fv_trm_open_trm_wrt_trm_upper :
L1 L2,
  fv_trm (open_trm_wrt_trm L1 L2) [<=] fv_trm L2 `union` fv_trm L1.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve fv_trm_open_trm_wrt_trm_upper : lngen.

Lemma fv_itrm_open_itrm_wrt_itrm_upper :
iL1 iL2,
  fv_itrm (open_itrm_wrt_itrm iL1 iL2) [<=] fv_itrm iL2 `union` fv_itrm iL1.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve fv_itrm_open_itrm_wrt_itrm_upper : lngen.


Lemma fv_trm_subst_trm_fresh :
L1 L2 x1,
  x1 `notin` fv_trm L1
  fv_trm (subst_trm L2 x1 L1) [=] fv_trm L1.
Proof.
pose proof fv_trm_subst_trm_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_trm_subst_trm_fresh : lngen.
Hint Rewrite fv_trm_subst_trm_fresh using solve [auto] : lngen.


Lemma fv_itrm_subst_itrm_fresh :
iL1 iL2 ix1,
  ix1 `notin` fv_itrm iL1
  fv_itrm (subst_itrm iL2 ix1 iL1) [=] fv_itrm iL1.
Proof.
pose proof fv_itrm_subst_itrm_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_itrm_subst_itrm_fresh : lngen.
Hint Rewrite fv_itrm_subst_itrm_fresh using solve [auto] : lngen.


Lemma fv_trm_subst_trm_lower :
L1 L2 x1,
  remove x1 (fv_trm L1) [<=] fv_trm (subst_trm L2 x1 L1).
Proof.
pose proof fv_trm_subst_trm_lower_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_trm_subst_trm_lower : lngen.


Lemma fv_itrm_subst_itrm_lower :
iL1 iL2 ix1,
  remove ix1 (fv_itrm iL1) [<=] fv_itrm (subst_itrm iL2 ix1 iL1).
Proof.
pose proof fv_itrm_subst_itrm_lower_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_itrm_subst_itrm_lower : lngen.


Lemma fv_trm_subst_trm_notin :
L1 L2 x1 x2,
  x2 `notin` fv_trm L1
  x2 `notin` fv_trm L2
  x2 `notin` fv_trm (subst_trm L2 x1 L1).
Proof.
pose proof fv_trm_subst_trm_notin_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_trm_subst_trm_notin : lngen.


Lemma fv_itrm_subst_itrm_notin :
iL1 iL2 ix1 ix2,
  ix2 `notin` fv_itrm iL1
  ix2 `notin` fv_itrm iL2
  ix2 `notin` fv_itrm (subst_itrm iL2 ix1 iL1).
Proof.
pose proof fv_itrm_subst_itrm_notin_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_itrm_subst_itrm_notin : lngen.


Lemma fv_trm_subst_trm_upper :
L1 L2 x1,
  fv_trm (subst_trm L2 x1 L1) [<=] fv_trm L2 `union` remove x1 (fv_trm L1).
Proof.
pose proof fv_trm_subst_trm_upper_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_trm_subst_trm_upper : lngen.


Lemma fv_itrm_subst_itrm_upper :
iL1 iL2 ix1,
  fv_itrm (subst_itrm iL2 ix1 iL1) [<=] fv_itrm iL2 `union` remove ix1 (fv_itrm iL1).
Proof.
pose proof fv_itrm_subst_itrm_upper_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_itrm_subst_itrm_upper : lngen.

Theorems about subst


Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.


Lemma subst_trm_close_trm_wrt_trm_rec :
L2 L1 x1 x2 n1,
  degree_trm_wrt_trm n1 L1
  x1 x2
  x2 `notin` fv_trm L1
  subst_trm L1 x1 (close_trm_wrt_trm_rec n1 x2 L2) = close_trm_wrt_trm_rec n1 x2 (subst_trm L1 x1 L2).
Proof.
pose proof subst_trm_close_trm_wrt_trm_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_close_trm_wrt_trm_rec : lngen.


Lemma subst_itrm_close_itrm_wrt_itrm_rec :
iL2 iL1 ix1 ix2 n1,
  degree_itrm_wrt_itrm n1 iL1
  ix1 ix2
  ix2 `notin` fv_itrm iL1
  subst_itrm iL1 ix1 (close_itrm_wrt_itrm_rec n1 ix2 iL2) = close_itrm_wrt_itrm_rec n1 ix2 (subst_itrm iL1 ix1 iL2).
Proof.
pose proof subst_itrm_close_itrm_wrt_itrm_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_close_itrm_wrt_itrm_rec : lngen.

Lemma subst_trm_close_trm_wrt_trm :
L2 L1 x1 x2,
  lc_trm L1 x1 x2
  x2 `notin` fv_trm L1
  subst_trm L1 x1 (close_trm_wrt_trm x2 L2) = close_trm_wrt_trm x2 (subst_trm L1 x1 L2).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_close_trm_wrt_trm : lngen.

Lemma subst_itrm_close_itrm_wrt_itrm :
iL2 iL1 ix1 ix2,
  lc_itrm iL1 ix1 ix2
  ix2 `notin` fv_itrm iL1
  subst_itrm iL1 ix1 (close_itrm_wrt_itrm ix2 iL2) = close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 iL2).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_close_itrm_wrt_itrm : lngen.


Lemma subst_trm_degree_trm_wrt_trm :
L1 L2 x1 n1,
  degree_trm_wrt_trm n1 L1
  degree_trm_wrt_trm n1 L2
  degree_trm_wrt_trm n1 (subst_trm L2 x1 L1).
Proof.
pose proof subst_trm_degree_trm_wrt_trm_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_degree_trm_wrt_trm : lngen.


Lemma subst_itrm_degree_itrm_wrt_itrm :
iL1 iL2 ix1 n1,
  degree_itrm_wrt_itrm n1 iL1
  degree_itrm_wrt_itrm n1 iL2
  degree_itrm_wrt_itrm n1 (subst_itrm iL2 ix1 iL1).
Proof.
pose proof subst_itrm_degree_itrm_wrt_itrm_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_degree_itrm_wrt_itrm : lngen.


Lemma subst_trm_fresh_eq :
L2 L1 x1,
  x1 `notin` fv_trm L2
  subst_trm L1 x1 L2 = L2.
Proof.
pose proof subst_trm_fresh_eq_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_fresh_eq : lngen.
Hint Rewrite subst_trm_fresh_eq using solve [auto] : lngen.


Lemma subst_itrm_fresh_eq :
iL2 iL1 ix1,
  ix1 `notin` fv_itrm iL2
  subst_itrm iL1 ix1 iL2 = iL2.
Proof.
pose proof subst_itrm_fresh_eq_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_fresh_eq : lngen.
Hint Rewrite subst_itrm_fresh_eq using solve [auto] : lngen.


Lemma subst_trm_fresh_same :
L2 L1 x1,
  x1 `notin` fv_trm L1
  x1 `notin` fv_trm (subst_trm L1 x1 L2).
Proof.
pose proof subst_trm_fresh_same_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_fresh_same : lngen.


Lemma subst_itrm_fresh_same :
iL2 iL1 ix1,
  ix1 `notin` fv_itrm iL1
  ix1 `notin` fv_itrm (subst_itrm iL1 ix1 iL2).
Proof.
pose proof subst_itrm_fresh_same_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_fresh_same : lngen.


Lemma subst_trm_fresh :
L2 L1 x1 x2,
  x1 `notin` fv_trm L2
  x1 `notin` fv_trm L1
  x1 `notin` fv_trm (subst_trm L1 x2 L2).
Proof.
pose proof subst_trm_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_fresh : lngen.


Lemma subst_itrm_fresh :
iL2 iL1 ix1 ix2,
  ix1 `notin` fv_itrm iL2
  ix1 `notin` fv_itrm iL1
  ix1 `notin` fv_itrm (subst_itrm iL1 ix2 iL2).
Proof.
pose proof subst_itrm_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_fresh : lngen.

Lemma subst_trm_lc_trm :
L1 L2 x1,
  lc_trm L1
  lc_trm L2
  lc_trm (subst_trm L2 x1 L1).
Proof.
default_simp.
Qed.

Hint Resolve subst_trm_lc_trm : lngen.

Lemma subst_itrm_lc_itrm :
iL1 iL2 ix1,
  lc_itrm iL1
  lc_itrm iL2
  lc_itrm (subst_itrm iL2 ix1 iL1).
Proof.
default_simp.
Qed.

Hint Resolve subst_itrm_lc_itrm : lngen.





Lemma subst_trm_open_trm_wrt_trm :
L3 L1 L2 x1,
  lc_trm L1
  subst_trm L1 x1 (open_trm_wrt_trm L3 L2) = open_trm_wrt_trm (subst_trm L1 x1 L3) (subst_trm L1 x1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_open_trm_wrt_trm : lngen.

Lemma subst_itrm_open_itrm_wrt_itrm :
iL3 iL1 iL2 ix1,
  lc_itrm iL1
  subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL3 iL2) = open_itrm_wrt_itrm (subst_itrm iL1 ix1 iL3) (subst_itrm iL1 ix1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_open_itrm_wrt_itrm : lngen.

Lemma subst_trm_open_trm_wrt_trm_var :
L2 L1 x1 x2,
  x1 x2
  lc_trm L1
  open_trm_wrt_trm (subst_trm L1 x1 L2) (t_var_f x2) = subst_trm L1 x1 (open_trm_wrt_trm L2 (t_var_f x2)).
Proof.
intros; rewrite subst_trm_open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_open_trm_wrt_trm_var : lngen.

Lemma subst_itrm_open_itrm_wrt_itrm_var :
iL2 iL1 ix1 ix2,
  ix1 ix2
  lc_itrm iL1
  open_itrm_wrt_itrm (subst_itrm iL1 ix1 iL2) (itrm_var_f ix2) = subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL2 (itrm_var_f ix2)).
Proof.
intros; rewrite subst_itrm_open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_open_itrm_wrt_itrm_var : lngen.





Lemma subst_trm_spec :
L1 L2 x1,
  subst_trm L2 x1 L1 = open_trm_wrt_trm (close_trm_wrt_trm x1 L1) L2.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_spec : lngen.

Lemma subst_itrm_spec :
iL1 iL2 ix1,
  subst_itrm iL2 ix1 iL1 = open_itrm_wrt_itrm (close_itrm_wrt_itrm ix1 iL1) iL2.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_spec : lngen.


Lemma subst_trm_subst_trm :
L1 L2 L3 x2 x1,
  x2 `notin` fv_trm L2
  x2 x1
  subst_trm L2 x1 (subst_trm L3 x2 L1) = subst_trm (subst_trm L2 x1 L3) x2 (subst_trm L2 x1 L1).
Proof.
pose proof subst_trm_subst_trm_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_subst_trm : lngen.


Lemma subst_itrm_subst_itrm :
iL1 iL2 iL3 ix2 ix1,
  ix2 `notin` fv_itrm iL2
  ix2 ix1
  subst_itrm iL2 ix1 (subst_itrm iL3 ix2 iL1) = subst_itrm (subst_itrm iL2 ix1 iL3) ix2 (subst_itrm iL2 ix1 iL1).
Proof.
pose proof subst_itrm_subst_itrm_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_subst_itrm : lngen.





Lemma subst_trm_close_trm_wrt_trm_open_trm_wrt_trm :
L2 L1 x1 x2,
  x2 `notin` fv_trm L2
  x2 `notin` fv_trm L1
  x2 x1
  lc_trm L1
  subst_trm L1 x1 L2 = close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm L2 (t_var_f x2))).
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_close_trm_wrt_trm_open_trm_wrt_trm : lngen.

Lemma subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm :
iL2 iL1 ix1 ix2,
  ix2 `notin` fv_itrm iL2
  ix2 `notin` fv_itrm iL1
  ix2 ix1
  lc_itrm iL1
  subst_itrm iL1 ix1 iL2 = close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL2 (itrm_var_f ix2))).
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.

Lemma subst_trm_t_abs :
x2 A1 N1 L1 x1,
  lc_trm L1
  x2 `notin` fv_trm L1 `union` fv_trm N1 `union` singleton x1
  subst_trm L1 x1 (t_abs A1 N1) = t_abs (A1) (close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm N1 (t_var_f x2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_trm_t_abs : lngen.

Lemma subst_trm_t_case :
x2 L2 M1 N1 L1 x1,
  lc_trm L1
  x2 `notin` fv_trm L1 `union` fv_trm N1 `union` singleton x1
  subst_trm L1 x1 (t_case L2 M1 N1) = t_case (subst_trm L1 x1 L2) (subst_trm L1 x1 M1) (close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm N1 (t_var_f x2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_trm_t_case : lngen.

Lemma subst_itrm_itrm_abs :
ix2 iA1 iN1 iL1 ix1,
  lc_itrm iL1
  ix2 `notin` fv_itrm iL1 `union` fv_itrm iN1 `union` singleton ix1
  subst_itrm iL1 ix1 (itrm_abs iA1 iN1) = itrm_abs (iA1) (close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 (open_itrm_wrt_itrm iN1 (itrm_var_f ix2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_itrm_itrm_abs : lngen.


Lemma subst_trm_intro_rec :
L1 x1 L2 n1,
  x1 `notin` fv_trm L1
  open_trm_wrt_trm_rec n1 L2 L1 = subst_trm L2 x1 (open_trm_wrt_trm_rec n1 (t_var_f x1) L1).
Proof.
pose proof subst_trm_intro_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_trm_intro_rec : lngen.
Hint Rewrite subst_trm_intro_rec using solve [auto] : lngen.


Lemma subst_itrm_intro_rec :
iL1 ix1 iL2 n1,
  ix1 `notin` fv_itrm iL1
  open_itrm_wrt_itrm_rec n1 iL2 iL1 = subst_itrm iL2 ix1 (open_itrm_wrt_itrm_rec n1 (itrm_var_f ix1) iL1).
Proof.
pose proof subst_itrm_intro_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_itrm_intro_rec : lngen.
Hint Rewrite subst_itrm_intro_rec using solve [auto] : lngen.

Lemma subst_trm_intro :
x1 L1 L2,
  x1 `notin` fv_trm L1
  open_trm_wrt_trm L1 L2 = subst_trm L2 x1 (open_trm_wrt_trm L1 (t_var_f x1)).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.

Hint Resolve subst_trm_intro : lngen.

Lemma subst_itrm_intro :
ix1 iL1 iL2,
  ix1 `notin` fv_itrm iL1
  open_itrm_wrt_itrm iL1 iL2 = subst_itrm iL2 ix1 (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.

Hint Resolve subst_itrm_intro : lngen.

"Restore" tactics


Ltac default_auto ::= auto; tauto.
Ltac default_autorewrite ::= fail.