From Tealeaves Require Export
  Examples.STLC.Syntax.

Import Syntax.TermNotations.

#[local] Open Scope set_scope.

Implicit Types (x: atom) (τ: typ)
  (t u: term) (n: nat) (v: LN) (Γ: ctx).

Ltac gather_atoms ::=
  let A := gather_atoms_with (fun s: AtomSet.t => s) in
  let B := gather_atoms_with (fun x: atom => {{ x }}) in
  let C := gather_atoms_with (fun t: term => FV t) in
  let D := gather_atoms_with (fun Γ: alist typ => domset Γ) in
  constr:(A ∪ B ∪ C ∪ D).

(** * Inversion lemmas *)
(**********************************************************************)
Lemma inversion11: forall (τ: typ) (x: atom) (Γ: ctx),
    Γ ⊢ tvar (Fr x): τ -> (x, τ) ∈ Γ.
forall τ x Γ, Γ ⊢ tvar x : τ -> (x, τ) ∈ Γ
Proof.
forall τ x Γ, Γ ⊢ tvar x : τ -> (x, τ) ∈ Γ
  inversion 1; auto.
Qed.

Lemma inversion12: forall (τ: typ) (n: nat) (Γ: ctx),
    Γ ⊢ tvar (Bd n): τ -> False.
forall τ n Γ, Γ ⊢ tvar n : τ -> False
Proof.
forall τ n Γ, Γ ⊢ tvar n : τ -> False
  inversion 1; auto.
Qed.

(* This is somewhat weak because L should really be (dom Γ) *)
Lemma inversion21: forall (τ B: typ) (e: term) (Γ: ctx),
    (Γ ⊢ λ τ e: B) ->
    exists C, B = τ ⟹ C /\ exists L, forall (x: atom),
        x `notin` L -> Γ ++ x ~ τ ⊢ e '(x): C.
forall (τ B : typ) (e : term) Γ,
Γ ⊢ (λ) τ e : B ->
exists C : typ,
  B = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x, x `notin` L -> Γ ++ x ~ τ ⊢ e '(x) : C)
Proof.
forall (τ B : typ) (e : term) Γ,
Γ ⊢ (λ) τ e : B ->
exists C : typ,
  B = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x, x `notin` L -> Γ ++ x ~ τ ⊢ e '(x) : C)
  introv J.
τ, B: typ
e: term
Γ: ctx
J: Γ ⊢ (λ) τ e : B
exists C : typ,
  B = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x,
     x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C)
  inversion J; subst.
τ: typ
e: term
Γ: ctx
τ2: typ
J: Γ ⊢ (λ) τ e : τ ⟹ τ2
L: AtomSet.t
H3: forall x,
x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ2
exists C : typ,
  τ ⟹ τ2 = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x,
     x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C)
  exists τ2.
τ: typ
e: term
Γ: ctx
τ2: typ
J: Γ ⊢ (λ) τ e : τ ⟹ τ2
L: AtomSet.t
H3: forall x,
x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ2
τ ⟹ τ2 = τ ⟹ τ2 /\
(exists L : AtomSet.t,
   forall x, x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ2) split; auto; exists L; auto.
Qed.

(** Inversion principle for [abs] where we may assume the abstraction has arrow type *)
Lemma inversion22: forall (τ τ': typ) (e: term) (Γ: ctx),
    Γ ⊢ λ τ e: τ ⟹ τ' ->
    exists L, forall (x: atom),
      x `notin` L ->
      Γ ++ x ~ τ ⊢ e '(x: term): τ'.
forall τ τ' (e : term) Γ,
Γ ⊢ (λ) τ e : τ ⟹ τ' ->
exists L : AtomSet.t,
  forall x,
  x `notin` L -> Γ ++ x ~ τ ⊢ e '(x : term) : τ'
Proof.
forall τ τ' (e : term) Γ,
Γ ⊢ (λ) τ e : τ ⟹ τ' ->
exists L : AtomSet.t,
  forall x,
  x `notin` L -> Γ ++ x ~ τ ⊢ e '(x : term) : τ'
  introv J.
τ, τ': typ
e: term
Γ: ctx
J: Γ ⊢ (λ) τ e : τ ⟹ τ'
exists L : AtomSet.t,
  forall x, x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ' apply inversion21 in J.
τ, τ': typ
e: term
Γ: ctx
J: exists C : typ,
  τ ⟹ τ' = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x,
     x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C)
exists L : AtomSet.t,
  forall x, x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ'
  destruct J as [C [H1 H2]].
τ, τ': typ
e: term
Γ: ctx
C: typ
H1: τ ⟹ τ' = τ ⟹ C
H2: exists L : AtomSet.t,
  forall x,
  x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C
exists L : AtomSet.t,
  forall x, x `notin` L -> Γ ++ x ~ τ ⊢ open x e : τ'
  assert (τ' = C) by (inversion H1; auto); subst.
τ: typ
e: term
Γ: ctx
C: typ
H1: τ ⟹ C = τ ⟹ C
H2: exists L : AtomSet.t,
  forall x,
  x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C
exists L : AtomSet.t,
  forall x, x `notin` L -> Γ ++ x ~ τ ⊢ open x e : C
  assumption.
Qed.

Lemma inversion3: forall (τ: typ) (Γ: ctx) (t1 t2: term),
    (Γ ⊢ ⟨t1⟩ (t2): τ) ->
    exists τ', (Γ ⊢ t1: τ' ⟹ τ)
          /\ (Γ ⊢ t2: τ').
forall τ Γ t1 t2,
Γ ⊢ ⟨ t1 ⟩ (t2) : τ ->
exists τ', (Γ ⊢ t1 : τ' ⟹ τ) /\ (Γ ⊢ t2 : τ')
Proof.
forall τ Γ t1 t2,
Γ ⊢ ⟨ t1 ⟩ (t2) : τ ->
exists τ', (Γ ⊢ t1 : τ' ⟹ τ) /\ (Γ ⊢ t2 : τ')
  introv J; inversion J; subst; eauto.
Qed.

(** * Misc lemmas *)
(**********************************************************************)
Theorem j_ctx_wf: forall Γ (t: term) (τ: typ),
    Γ ⊢ t: τ -> uniq Γ.
forall Γ t τ, Γ ⊢ t : τ -> uniq Γ
Proof.
forall Γ t τ, Γ ⊢ t : τ -> uniq Γ
  introv J; typing_induction.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
uniq Γ
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x, x `notin` L -> uniq (Γ ++ x ~ τ1)
uniq Γ
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1, IHJ2: uniq Γ
uniq Γ
  -
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
uniq Γ assumption.
  -
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x, x `notin` L -> uniq (Γ ++ x ~ τ1)
uniq Γ specialize_freshly IHbody.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: uniq (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
uniq Γ
    now autorewrite with tea_rw_uniq in IHbody.
  -
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1, IHJ2: uniq Γ
uniq Γ assumption.
Qed.

Theorem j_wf: forall Γ (t: term) (τ: typ),
    Γ ⊢ t: τ -> FV t ⊆ domset Γ.
forall Γ t τ, Γ ⊢ t : τ -> FV t ⊆ domset Γ
Proof.
forall Γ t τ, Γ ⊢ t : τ -> FV t ⊆ domset Γ
  introv J.
Γ: ctx
t: term
τ: typ
J: Γ ⊢ t : τ
FV t ⊆ domset Γ typing_induction.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
FV x ⊆ domset Γ
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x,
x `notin` L ->
FV (open x body) ⊆ domset (Γ ++ x ~ τ1)
FV ((λ) τ1 body) ⊆ domset Γ
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: FV t1 ⊆ domset Γ
IHJ2: FV t2 ⊆ domset Γ
FV (⟨ t1 ⟩ (t2)) ⊆ domset Γ
  -
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
FV x ⊆ domset Γ simplify_LN.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
{{x}} ⊆ domset Γ
    apply in_in_domset in Hin.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: x `in` domset Γ
{{x}} ⊆ domset Γ
    fsetdec.
  -
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x,
x `notin` L ->
FV (open x body) ⊆ domset (Γ ++ x ~ τ1)
FV ((λ) τ1 body) ⊆ domset Γ specialize_freshly IHbody.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
FV ((λ) τ1 body) ⊆ domset Γ
    simplify_LN.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
FV body ⊆ domset Γ
    assert (step1: FV body ⊆ FV (body '(e: term)))
      by apply (FV_open_lower (Binddt_TU := Binddt_STLC)).
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
FV body ⊆ domset Γ
    assert (step2: forall x, x `in` FV body -> x `in` (domset (Γ ++ e ~ τ1)))
      by fsetdec.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
step2: forall x,
x `in` FV body -> x `in` domset (Γ ++ e ~ τ1)
FV body ⊆ domset Γ
    intros x xin.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
step2: forall x,
x `in` FV body -> x `in` domset (Γ ++ e ~ τ1)
x: AtomSet.elt
xin: x `in` FV body
x `in` domset Γ
    assert (x <> e) by fsetdec.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
step2: forall x,
x `in` FV body -> x `in` domset (Γ ++ e ~ τ1)
x: AtomSet.elt
xin: x `in` FV body
H: x <> e
x `in` domset Γ
    specialize (step2 x xin).
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
x: AtomSet.elt
step2: x `in` domset (Γ ++ e ~ τ1)
xin: x `in` FV body
H: x <> e
x `in` domset Γ
    rewrite domset_app in step2.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
x: AtomSet.elt
step2: x `in` (domset Γ ∪ domset (e ~ τ1))
xin: x `in` FV body
H: x <> e
x `in` domset Γ
    rewrite domset_one in step2.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
e: atom
IHbody: FV (open e body) ⊆ domset (Γ ++ e ~ τ1)
Hfresh: e `notin` (L ∪ (FV body ∪ domset Γ))
step1: FV body ⊆ FV (body '(e : term))
x: AtomSet.elt
step2: x `in` (domset Γ ∪ {{e}})
xin: x `in` FV body
H: x <> e
x `in` domset Γ
    fsetdec.
  -
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: FV t1 ⊆ domset Γ
IHJ2: FV t2 ⊆ domset Γ
FV (⟨ t1 ⟩ (t2)) ⊆ domset Γ simplify_LN.
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: FV t1 ⊆ domset Γ
IHJ2: FV t2 ⊆ domset Γ
FV t1 ∪ FV t2 ⊆ domset Γ
    fsetdec.
Qed.

Theorem lc_lam: forall (L: AtomSet.t) (t: term) (X: typ),
    (forall x: atom, ~ x `in` L -> LC (t '(x: term))) ->
    LC (λ X t).
forall (L : AtomSet.t) t (X : typ),
(forall x, x `notin` L -> LC (t '(x : term))) ->
LC ((λ) X t)
Proof.
forall (L : AtomSet.t) t (X : typ),
(forall x, x `notin` L -> LC (t '(x : term))) ->
LC ((λ) X t)
  introv HLC.
L: AtomSet.t
t: term
X: typ
HLC: forall x, x `notin` L -> LC (open x t)
LC ((λ) X t)
  simplify_LN.
L: AtomSet.t
t: term
X: typ
HLC: forall x, x `notin` L -> LC (open x t)
LCn 1 t
  specialize_freshly HLC.
L: AtomSet.t
t: term
X: typ
e: atom
HLC: LC (open e t)
Hfresh: e `notin` (L ∪ FV t)
LCn 1 t
  change (fvar e) with (ret (Fr e)) in HLC.
L: AtomSet.t
t: term
X: typ
e: atom
HLC: LC (open (ret e) t)
Hfresh: e `notin` (L ∪ FV t)
LCn 1 t
  rewrite <- lc_open_var in HLC.
L: AtomSet.t
t: term
X: typ
e: atom
HLC: LCn 1 t
Hfresh: e `notin` (L ∪ FV t)
LCn 1 t
  assumption.
Qed.

Theorem j_lc: forall Γ t τ,
    Γ ⊢ t: τ -> LC t.
forall Γ t τ, Γ ⊢ t : τ -> LC t
Proof.
forall Γ t τ, Γ ⊢ t : τ -> LC t
  introv J.
Γ: ctx
t: term
τ: typ
J: Γ ⊢ t : τ
LC t typing_induction.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
LC x
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x, x `notin` L -> LC (open x body)
LC ((λ) τ1 body)
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: LC t1
IHJ2: LC t2
LC (⟨ t1 ⟩ (t2))
  -
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
LC x simplify_LN.
Γ: ctx
x: atom
τ0: typ
Huniq: uniq Γ
Hin: (x, τ0) ∈ Γ
True exact I.
  -
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x, x `notin` L -> LC (open x body)
LC ((λ) τ1 body) pick fresh y excluding L and apply lc_lam.
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x, x `notin` L -> LC (open x body)
y: atom
Fr: y `notin` L
LC (open y body)
    apply IHbody; auto.
  -
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: LC t1
IHJ2: LC t2
LC (⟨ t1 ⟩ (t2)) simplify_LN.
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: LC t1
IHJ2: LC t2
LC t1 ● LC t2 split; assumption.
Qed.

Theorem weakening: forall Γ1 Γ2 Γ' (t: term) (τ: typ),
    uniq Γ' ->
    disjoint Γ' (Γ1 ++ Γ2) ->
    (Γ1 ++ Γ2 ⊢ t: τ) ->
    (Γ1 ++ Γ' ++ Γ2 ⊢ t: τ).
forall Γ1 Γ2 Γ' t τ,
uniq Γ' ->
disjoint Γ' (Γ1 ++ Γ2) ->
Γ1 ++ Γ2 ⊢ t : τ -> Γ1 ++ Γ' ++ Γ2 ⊢ t : τ
Proof.
forall Γ1 Γ2 Γ' t τ,
uniq Γ' ->
disjoint Γ' (Γ1 ++ Γ2) ->
Γ1 ++ Γ2 ⊢ t : τ -> Γ1 ++ Γ' ++ Γ2 ⊢ t : τ
  introv Huq Hdj J.
Γ1, Γ2, Γ': ctx
t: term
τ: typ
Huq: uniq Γ'
Hdj: disjoint Γ' (Γ1 ++ Γ2)
J: Γ1 ++ Γ2 ⊢ t : τ
Γ1 ++ Γ' ++ Γ2 ⊢ t : τ
  remember (Γ1 ++ Γ2) as Γrem.
Γ1, Γ2, Γ': ctx
t: term
τ: typ
Huq: uniq Γ'
Γrem: list (atom * typ)
HeqΓrem: Γrem = Γ1 ++ Γ2
Hdj: disjoint Γ' Γrem
J: Γrem ⊢ t : τ
Γ1 ++ Γ' ++ Γ2 ⊢ t : τ
  generalize dependent Γ2.
Γ1, Γ': ctx
t: term
τ: typ
Huq: uniq Γ'
Γrem: list (atom * typ)
Hdj: disjoint Γ' Γrem
J: Γrem ⊢ t : τ
forall Γ2, Γrem = Γ1 ++ Γ2 -> Γ1 ++ Γ' ++ Γ2 ⊢ t : τ
  typing_induction; intros Γ2 HeqΓ; subst.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
Γ1 ++ Γ' ++ Γ2 ⊢ x : τ0
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
disjoint Γ' ((Γ1 ++ Γ2) ++ x ~ τ1) ->
forall Γ3,
(Γ1 ++ Γ2) ++ x ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open x body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Γ1 ++ Γ' ++ Γ2 ⊢ (λ) τ1 body : τ1 ⟹ τ2
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
t1, t2: term
τ1, τ2: typ
IHJ2: disjoint Γ' (Γ1 ++ Γ2) ->
forall Γ3,
Γ1 ++ Γ2 = Γ1 ++ Γ3 -> Γ1 ++ Γ' ++ Γ3 ⊢ t2 : τ1
IHJ1: disjoint Γ' (Γ1 ++ Γ2) ->
forall Γ3,
Γ1 ++ Γ2 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ t1 : τ1 ⟹ τ2
J2: Γ1 ++ Γ2 ⊢ t2 : τ1
J1: Γ1 ++ Γ2 ⊢ t1 : τ1 ⟹ τ2
Γ1 ++ Γ' ++ Γ2 ⊢ ⟨ t1 ⟩ (t2) : τ2
  -
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
Γ1 ++ Γ' ++ Γ2 ⊢ x : τ0 apply j_var.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
uniq (Γ1 ++ Γ' ++ Γ2)
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
(x, τ0) ∈ (Γ1 ++ Γ' ++ Γ2)
    {
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
uniq (Γ1 ++ Γ' ++ Γ2) autorewrite with tea_rw_uniq tea_rw_disj in *.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ1 Γ' /\ disjoint Γ2 Γ'
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
uniq Γ1 /\
(uniq Γ' /\ uniq Γ2 /\ disjoint Γ' Γ2) /\
disjoint Γ' Γ1 /\ disjoint Γ2 Γ1
      rewrite disjoint_sym.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ1 Γ' /\ disjoint Γ2 Γ'
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
uniq Γ1 /\
(uniq Γ' /\ uniq Γ2 /\ disjoint Γ2 Γ') /\
disjoint Γ' Γ1 /\ disjoint Γ2 Γ1
      preprocess; intuition. }
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ (Γ1 ++ Γ2)
Huniq: uniq (Γ1 ++ Γ2)
(x, τ0) ∈ (Γ1 ++ Γ' ++ Γ2)
    simpl_list in *.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
x: atom
τ0: typ
Hin: (x, τ0) ∈ Γ1 \/ (x, τ0) ∈ Γ2
Huniq: uniq (Γ1 ++ Γ2)
(x, τ0) ∈ Γ1 \/ (x, τ0) ∈ Γ' \/ (x, τ0) ∈ Γ2
    intuition.
  -
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
disjoint Γ' ((Γ1 ++ Γ2) ++ x ~ τ1) ->
forall Γ3,
(Γ1 ++ Γ2) ++ x ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open x body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Γ1 ++ Γ' ++ Γ2 ⊢ (λ) τ1 body : τ1 ⟹ τ2 pick fresh y and apply j_abs.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
disjoint Γ' ((Γ1 ++ Γ2) ++ x ~ τ1) ->
forall Γ3,
(Γ1 ++ Γ2) ++ x ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open x body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
y: atom
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
(Γ1 ++ Γ' ++ Γ2) ++ y ~ τ1 ⊢ open y body : τ2
    specialize_cof IHbody y.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' ((Γ1 ++ Γ2) ++ y ~ τ1) ->
forall Γ3,
(Γ1 ++ Γ2) ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
(Γ1 ++ Γ' ++ Γ2) ++ y ~ τ1 ⊢ open y body : τ2
    simpl_alist in IHbody.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
(Γ1 ++ Γ' ++ Γ2) ++ y ~ τ1 ⊢ open y body : τ2
    simpl_alist.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
Γ1 ++ Γ' ++ Γ2 ++ y ~ τ1 ⊢ open y body : τ2
    apply IHbody.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1)
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ2 ++ y ~ τ1
    {
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) autorewrite with tea_rw_disj in *.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ1 Γ' /\ disjoint Γ2 Γ'
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ1 Γ' /\
disjoint Γ2 Γ' /\ y `notin` domset Γ' ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
disjoint Γ1 Γ' /\
disjoint Γ2 Γ' /\ y `notin` domset Γ'
      splits; try easy.
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ1 Γ' /\ disjoint Γ2 Γ'
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ1 Γ' /\
disjoint Γ2 Γ' /\ y `notin` domset Γ' ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
y `notin` domset Γ' fsetdec. }
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ2 ++ y ~ τ1
    {
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
L: AtomSet.t
τ1, τ2: typ
body: term
y: atom
IHbody: disjoint Γ' (Γ1 ++ Γ2 ++ y ~ τ1) ->
forall Γ3,
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ open y body : τ2
Jbody: forall x,
x `notin` L ->
(Γ1 ++ Γ2) ++ x ~ τ1 ⊢ open x body : τ2
Fr: y
`notin` (L
         ∪ (FV body
            ∪ (domset Γ1
               ∪ (domset Γ' ∪ domset Γ2))))
Γ1 ++ Γ2 ++ y ~ τ1 = Γ1 ++ Γ2 ++ y ~ τ1 reflexivity. }
  -
Γ1, Γ': ctx
Huq: uniq Γ'
Γ2: ctx
Hdj: disjoint Γ' (Γ1 ++ Γ2)
t1, t2: term
τ1, τ2: typ
IHJ2: disjoint Γ' (Γ1 ++ Γ2) ->
forall Γ3,
Γ1 ++ Γ2 = Γ1 ++ Γ3 -> Γ1 ++ Γ' ++ Γ3 ⊢ t2 : τ1
IHJ1: disjoint Γ' (Γ1 ++ Γ2) ->
forall Γ3,
Γ1 ++ Γ2 = Γ1 ++ Γ3 ->
Γ1 ++ Γ' ++ Γ3 ⊢ t1 : τ1 ⟹ τ2
J2: Γ1 ++ Γ2 ⊢ t2 : τ1
J1: Γ1 ++ Γ2 ⊢ t1 : τ1 ⟹ τ2
Γ1 ++ Γ' ++ Γ2 ⊢ ⟨ t1 ⟩ (t2) : τ2 eauto using j_app.
Qed.

Corollary weakening_r: forall Γ1 (t: term) (τ: typ),
    (Γ1 ⊢ t: τ) ->
    forall Γ2, uniq Γ2 -> disjoint Γ1 Γ2 -> Γ1 ++ Γ2 ⊢ t: τ.
forall Γ1 t τ,
Γ1 ⊢ t : τ ->
forall Γ2,
uniq Γ2 -> disjoint Γ1 Γ2 -> Γ1 ++ Γ2 ⊢ t : τ
Proof.
forall Γ1 t τ,
Γ1 ⊢ t : τ ->
forall Γ2,
uniq Γ2 -> disjoint Γ1 Γ2 -> Γ1 ++ Γ2 ⊢ t : τ
  intros.
Γ1: ctx
t: term
τ: typ
H: Γ1 ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
Γ1 ++ Γ2 ⊢ t : τ
  rewrite <- (List.app_nil_r Γ1) in H.
Γ1: ctx
t: term
τ: typ
H: Γ1 ++ [] ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
Γ1 ++ Γ2 ⊢ t : τ
  rewrite <- (List.app_nil_r (Γ1 ++ Γ2)).
Γ1: ctx
t: term
τ: typ
H: Γ1 ++ [] ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(Γ1 ++ Γ2) ++ [] ⊢ t : τ
  rewrite <- List.app_assoc.
Γ1: ctx
t: term
τ: typ
H: Γ1 ++ [] ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
Γ1 ++ Γ2 ++ [] ⊢ t : τ
  apply weakening; auto.
Γ1: ctx
t: term
τ: typ
H: Γ1 ++ [] ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
disjoint Γ2 (Γ1 ++ [])
  List.simpl_list.
Γ1: ctx
t: term
τ: typ
H: Γ1 ++ [] ⊢ t : τ
Γ2: ctx
H0: uniq Γ2
H1: disjoint Γ1 Γ2
disjoint Γ2 Γ1
  eauto with tea_alist.
Qed.

Theorem substitution: forall Γ1 Γ2 x t u τ1 τ2,
    (Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t: τ2) ->
    (Γ1 ⊢ u: τ1) ->
    Γ1 ++ Γ2 ⊢ t '{x ~> u}: τ2.
forall Γ1 Γ2 x t u τ1 τ2,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ2 ->
Γ1 ⊢ u : τ1 -> Γ1 ++ Γ2 ⊢ t '{ x ~> u} : τ2
Proof.
forall Γ1 Γ2 x t u τ1 τ2,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ2 ->
Γ1 ⊢ u : τ1 -> Γ1 ++ Γ2 ⊢ t '{ x ~> u} : τ2
  introv Jt Ju.
Γ1, Γ2: ctx
x: atom
t, u: term
τ1, τ2: typ
Jt: Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ2
Ju: Γ1 ⊢ u : τ1
Γ1 ++ Γ2 ⊢ subst x u t : τ2
  specialize (j_ctx_wf (Γ1 ++ x ~ τ1 ++ Γ2)); intro Hwf.
Γ1, Γ2: ctx
x: atom
t, u: term
τ1, τ2: typ
Jt: Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ2
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ -> uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Γ1 ++ Γ2 ⊢ subst x u t : τ2
  assert (LC u) by (eauto using j_lc).
Γ1, Γ2: ctx
x: atom
t, u: term
τ1, τ2: typ
Jt: Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ2
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ -> uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
Γ1 ++ Γ2 ⊢ subst x u t : τ2
  remember (Γ1 ++ x ~ τ1 ++ Γ2) as Γrem.
Γ1, Γ2: ctx
x: atom
t, u: term
τ1, τ2: typ
Γrem: list (atom * typ)
HeqΓrem: Γrem = Γ1 ++ x ~ τ1 ++ Γ2
Jt: Γrem ⊢ t : τ2
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γrem ⊢ t : τ -> uniq Γrem
H: LC u
Γ1 ++ Γ2 ⊢ subst x u t : τ2
  generalize dependent Γ2.
Γ1: ctx
x: atom
t, u: term
τ1, τ2: typ
Γrem: list (atom * typ)
Jt: Γrem ⊢ t : τ2
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γrem ⊢ t : τ -> uniq Γrem
H: LC u
forall Γ2,
Γrem = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t : τ2
  typing_induction_on Jt; intros Γ2 HeqΓ.
Γ1: ctx
x: atom
u: term
τ1: typ
Γ: ctx
x0: atom
τ: typ
Huniq: uniq Γ
Hin: (x0, τ) ∈ Γ
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u x0 : τ
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
IHbody: forall x0,
x0 `notin` L ->
(forall t τ,
 Γ ++ x0 ~ τ0 ⊢ t : τ -> uniq (Γ ++ x0 ~ τ0)) ->
forall Γ2,
Γ ++ x0 ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open x0 body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u ((λ) τ0 body) : τ0 ⟹ τ3
Γ1: ctx
x: atom
u: term
τ1: typ
Γ: ctx
t1, t2: term
τ0, τ3: typ
J1: Γ ⊢ t1 : τ0 ⟹ τ3
J2: Γ ⊢ t2 : τ0
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
IHJ1: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t1 : τ0 ⟹ τ3
IHJ2: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t2 : τ0
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u (⟨ t1 ⟩ (t2)) : τ3
  -
Γ1: ctx
x: atom
u: term
τ1: typ
Γ: ctx
x0: atom
τ: typ
Huniq: uniq Γ
Hin: (x0, τ) ∈ Γ
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u x0 : τ compare values x and x0.
Γ1: ctx
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ++ Γ2 ⊢ subst x0 u x0 : τ
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
Γ1 ++ Γ2 ⊢ subst x u x0 : τ
    +
Γ1: ctx
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ++ Γ2 ⊢ subst x0 u x0 : τ simplify_subst.
Γ1: ctx
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ++ Γ2 ⊢ (if x0 == x0 then u else ret x0) : τ
      simpl_local.
Γ1: ctx
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ++ Γ2 ⊢ (if x0 == x0 then u else ret x0) : τ
      assert (τ = τ1) by eauto using binds_mid_eq; subst.
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ++ Γ2 ⊢ (if x0 == x0 then u else ret x0) : τ1
      apply weakening_r.
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ⊢ (if x0 == x0 then u else ret x0) : τ1
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
uniq Γ2
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
disjoint Γ1 Γ2
      {
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
Γ1 ⊢ (if x0 == x0 then u else ret x0) : τ1 compare values x0 and x0. }
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
uniq Γ2
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
disjoint Γ1 Γ2
      {
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
uniq Γ2 autorewrite with tea_rw_uniq tea_rw_disj in *.
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq Γ1 /\
(True /\ uniq Γ2 /\ x0 `notin` domset Γ2) /\
x0 `notin` domset Γ1 /\ disjoint Γ2 Γ1
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
uniq Γ2
        intuition. }
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
disjoint Γ1 Γ2
      {
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
disjoint Γ1 Γ2 autorewrite with tea_rw_uniq tea_rw_disj in *.
Γ1: ctx
u: term
τ1: typ
x0: atom
Γ2: ctx
Huniq: uniq Γ1 /\
(True /\ uniq Γ2 /\ x0 `notin` domset Γ2) /\
x0 `notin` domset Γ1 /\ disjoint Γ2 Γ1
Hin: (x0, τ1) ∈ (Γ1 ++ x0 ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x0 ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x0 ~ τ1 ++ Γ2)
H: LC u
DESTR_EQs: x0 = x0
disjoint Γ1 Γ2
        intuition. }
    +
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
Γ1 ++ Γ2 ⊢ subst x u x0 : τ simplify_LN.
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
Γ1 ++ Γ2 ⊢ ret x0 : τ apply j_var.
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
uniq (Γ1 ++ Γ2)
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
(x0, τ) ∈ (Γ1 ++ Γ2)
      {
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
uniq (Γ1 ++ Γ2) autorewrite with tea_rw_uniq tea_rw_disj in *.
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
        intuition. }
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
(x0, τ) ∈ (Γ1 ++ Γ2)
      {
Γ1: ctx
x: atom
u: term
τ1: typ
x0: atom
τ: typ
Γ2: ctx
Hin: (x0, τ) ∈ (Γ1 ++ x ~ τ1 ++ Γ2)
Huniq: uniq (Γ1 ++ x ~ τ1 ++ Γ2)
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
(x0, τ) ∈ (Γ1 ++ Γ2) eauto using binds_remove_mid. }
  -
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
IHbody: forall x0,
x0 `notin` L ->
(forall t τ,
 Γ ++ x0 ~ τ0 ⊢ t : τ -> uniq (Γ ++ x0 ~ τ0)) ->
forall Γ2,
Γ ++ x0 ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open x0 body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u ((λ) τ0 body) : τ0 ⟹ τ3 simplify_subst.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
IHbody: forall x0,
x0 `notin` L ->
(forall t τ,
 Γ ++ x0 ~ τ0 ⊢ t : τ -> uniq (Γ ++ x0 ~ τ0)) ->
forall Γ2,
Γ ++ x0 ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open x0 body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ (λ) τ0 (subst x u body) : τ0 ⟹ τ3
    apply j_abs with (L := L ∪ domset Γ ∪ {{x}}).
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
IHbody: forall x0,
x0 `notin` L ->
(forall t τ,
 Γ ++ x0 ~ τ0 ⊢ t : τ -> uniq (Γ ++ x0 ~ τ0)) ->
forall Γ2,
Γ ++ x0 ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open x0 body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
forall x0,
x0 `notin` (L ∪ domset Γ ∪ {{x}}) ->
(Γ1 ++ Γ2) ++ x0 ~ τ0 ⊢ open x0 (subst x u body) : τ3
    intros_cof IHbody.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
(Γ1 ++ Γ2) ++ e ~ τ0 ⊢ open e (subst x u body) : τ3
    change (fvar e) with (ret (Fr e)).
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
(Γ1 ++ Γ2) ++ e ~ τ0 ⊢ open (ret e) (subst x u body)
: τ3
    rewrite <- subst_open_var.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
(Γ1 ++ Γ2) ++ e ~ τ0 ⊢ subst x u (open (ret e) body)
: τ3
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
x <> e
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
LC u
    +
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
(Γ1 ++ Γ2) ++ e ~ τ0 ⊢ subst x u (open (ret e) body)
: τ3 simpl_alist in *.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
Γ1 ++ Γ2 ++ e ~ τ0 ⊢ subst x u (open (ret e) body)
: τ3
      eapply IHbody.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
forall t τ, Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ++ e ~ τ0
      *
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
forall t τ, Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0) eauto using j_ctx_wf.
      *
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ++ e ~ τ0 subst.
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
τ0, τ3: typ
body: term
Γ2: ctx
Jbody: forall x0,
x0 `notin` L ->
(Γ1 ++ x ~ τ1 ++ Γ2) ++ x0 ~ τ0 ⊢ 
open x0 body : τ3
e: atom
IHbody: (forall t τ,
 (Γ1 ++ x ~ τ1 ++ Γ2) ++ e ~ τ0 ⊢ t : τ ->
 uniq ((Γ1 ++ x ~ τ1 ++ Γ2) ++ e ~ τ0)) ->
forall Γ3,
(Γ1 ++ x ~ τ1 ++ Γ2) ++ e ~ τ0 =
Γ1 ++ x ~ τ1 ++ Γ3 ->
Γ1 ++ Γ3 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ,
Γ1 ++ x ~ τ1 ++ Γ2 ⊢ t : τ ->
uniq (Γ1 ++ x ~ τ1 ++ Γ2)
H: LC u
Notin: e
`notin` (L ∪ domset (Γ1 ++ x ~ τ1 ++ Γ2)
         ∪ {{x}})
(Γ1 ++ x ~ τ1 ++ Γ2) ++ e ~ τ0 =
Γ1 ++ x ~ τ1 ++ Γ2 ++ e ~ τ0 now simpl_alist.
    +
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
x <> e fsetdec.
    +
Γ1: ctx
x: atom
u: term
τ1: typ
L: AtomSet.t
Γ: ctx
τ0, τ3: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ0 ⊢ open x body : τ3
e: atom
IHbody: (forall t τ,
 Γ ++ e ~ τ0 ⊢ t : τ -> uniq (Γ ++ e ~ τ0)) ->
forall Γ2,
Γ ++ e ~ τ0 = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u (open e body) : τ3
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Notin: e `notin` (L ∪ domset Γ ∪ {{x}})
LC u auto.
  -
Γ1: ctx
x: atom
u: term
τ1: typ
Γ: ctx
t1, t2: term
τ0, τ3: typ
J1: Γ ⊢ t1 : τ0 ⟹ τ3
J2: Γ ⊢ t2 : τ0
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
IHJ1: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t1 : τ0 ⟹ τ3
IHJ2: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t2 : τ0
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ subst x u (⟨ t1 ⟩ (t2)) : τ3 simplify_LN.
Γ1: ctx
x: atom
u: term
τ1: typ
Γ: ctx
t1, t2: term
τ0, τ3: typ
J1: Γ ⊢ t1 : τ0 ⟹ τ3
J2: Γ ⊢ t2 : τ0
Ju: Γ1 ⊢ u : τ1
Hwf: forall t τ, Γ ⊢ t : τ -> uniq Γ
H: LC u
IHJ1: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t1 : τ0 ⟹ τ3
IHJ2: (forall t τ, Γ ⊢ t : τ -> uniq Γ) ->
forall Γ2,
Γ = Γ1 ++ x ~ τ1 ++ Γ2 ->
Γ1 ++ Γ2 ⊢ subst x u t2 : τ0
Γ2: ctx
HeqΓ: Γ = Γ1 ++ x ~ τ1 ++ Γ2
Γ1 ++ Γ2 ⊢ ⟨ subst x u t1 ⟩ (subst x u t2) : τ3 eauto using j_app.
Qed.

Corollary substitution_r: forall Γ (x: atom) (t u: term) (A B: typ),
    (Γ ++ x ~ A ⊢ t: B) ->
    (Γ ⊢ u: A) ->
    (Γ ⊢ t '{x ~> u}: B).
forall Γ x t u (A B : typ),
Γ ++ x ~ A ⊢ t : B ->
Γ ⊢ u : A -> Γ ⊢ t '{ x ~> u} : B
Proof.
forall Γ x t u (A B : typ),
Γ ++ x ~ A ⊢ t : B ->
Γ ⊢ u : A -> Γ ⊢ t '{ x ~> u} : B
  introv Jt Ju.
Γ: ctx
x: atom
t, u: term
A, B: typ
Jt: Γ ++ x ~ A ⊢ t : B
Ju: Γ ⊢ u : A
Γ ⊢ subst x u t : B
  change_alist (Γ ++ x ~ A ++ nil) in Jt.
Γ: ctx
x: atom
t, u: term
A, B: typ
Jt: Γ ++ x ~ A ++ [] ⊢ t : B
Ju: Γ ⊢ u : A
Γ ⊢ subst x u t : B
  change_alist (Γ ++ nil).
Γ: ctx
x: atom
t, u: term
A, B: typ
Jt: Γ ++ x ~ A ++ [] ⊢ t : B
Ju: Γ ⊢ u : A
Γ ++ [] ⊢ subst x u t : B
  eapply substitution; eauto.
Qed.

Inductive value: term -> Prop :=
  | value_abs: forall X t, value (λ X t).

Inductive beta_step: term -> term -> Prop :=
| beta_app_l: forall (t1 t2 t1': term),
    beta_step t1 t1' ->
    beta_step (⟨t1⟩ (t2)) (⟨t1'⟩(t2))
| beta_app_r: forall (t1 t2 t2': term),
    beta_step t2 t2' ->
    beta_step (⟨t1⟩(t2)) (⟨t1⟩(t2'))
| beta_beta: forall τ t u,
    beta_step (⟨λ τ t⟩(u)) (t '(u)).

Theorem subject_reduction_step: forall (t t': term) Γ A,
    Γ ⊢ t: A -> beta_step t t' -> Γ ⊢ t': A.
forall t t' Γ (A : typ),
Γ ⊢ t : A -> beta_step t t' -> Γ ⊢ t' : A
Proof.
forall t t' Γ (A : typ),
Γ ⊢ t : A -> beta_step t t' -> Γ ⊢ t' : A
  introv J Hstep.
t, t': term
Γ: ctx
A: typ
J: Γ ⊢ t : A
Hstep: beta_step t t'
Γ ⊢ t' : A
  generalize dependent t'.
t: term
Γ: ctx
A: typ
J: Γ ⊢ t : A
forall t', beta_step t t' -> Γ ⊢ t' : A
  typing_induction; intros t' Hstep.
Γ: ctx
x: atom
τ: typ
Huniq: uniq Γ
Hin: (x, τ) ∈ Γ
t': term
Hstep: beta_step x t'
Γ ⊢ t' : τ
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x,
x `notin` L ->
forall t',
beta_step (open x body) t' ->
Γ ++ x ~ τ1 ⊢ t' : τ2
t': term
Hstep: beta_step ((λ) τ1 body) t'
Γ ⊢ t' : τ1 ⟹ τ2
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
Γ ⊢ t' : τ2
  -
Γ: ctx
x: atom
τ: typ
Huniq: uniq Γ
Hin: (x, τ) ∈ Γ
t': term
Hstep: beta_step x t'
Γ ⊢ t' : τ inversion Hstep.
  -
L: AtomSet.t
Γ: ctx
τ1, τ2: typ
body: term
Jbody: forall x,
x `notin` L -> Γ ++ x ~ τ1 ⊢ open x body : τ2
IHbody: forall x,
x `notin` L ->
forall t',
beta_step (open x body) t' ->
Γ ++ x ~ τ1 ⊢ t' : τ2
t': term
Hstep: beta_step ((λ) τ1 body) t'
Γ ⊢ t' : τ1 ⟹ τ2 inversion Hstep.
  -
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
Γ ⊢ t' : τ2 inversion Hstep.
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
t0, t3, t1': term
H2: beta_step t1 t1'
H: t0 = t1
H1: t3 = t2
H0: (⟨ t1' ⟩ (t2)) = t'
Γ ⊢ ⟨ t1' ⟩ (t2) : τ2
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
t0, t3, t2': term
H2: beta_step t2 t2'
H: t0 = t1
H1: t3 = t2
H0: (⟨ t1 ⟩ (t2')) = t'
Γ ⊢ ⟨ t1 ⟩ (t2') : τ2
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
τ: typ
t, u: term
H0: (λ) τ t = t1
H1: u = t2
H2: open t2 t = t'
Γ ⊢ open t2 t : τ2
    +
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
t0, t3, t1': term
H2: beta_step t1 t1'
H: t0 = t1
H1: t3 = t2
H0: (⟨ t1' ⟩ (t2)) = t'
Γ ⊢ ⟨ t1' ⟩ (t2) : τ2 subst.
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t1': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) (⟨ t1' ⟩ (t2))
H2: beta_step t1 t1'
Γ ⊢ ⟨ t1' ⟩ (t2) : τ2 eauto using j_app.
    +
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
t0, t3, t2': term
H2: beta_step t2 t2'
H: t0 = t1
H1: t3 = t2
H0: (⟨ t1 ⟩ (t2')) = t'
Γ ⊢ ⟨ t1 ⟩ (t2') : τ2 subst.
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t2': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) (⟨ t1 ⟩ (t2'))
H2: beta_step t2 t2'
Γ ⊢ ⟨ t1 ⟩ (t2') : τ2 eauto using j_app.
    +
Γ: ctx
t1, t2: term
τ1, τ2: typ
J1: Γ ⊢ t1 : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t', beta_step t1 t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
t': term
Hstep: beta_step (⟨ t1 ⟩ (t2)) t'
τ: typ
t, u: term
H0: (λ) τ t = t1
H1: u = t2
H2: open t2 t = t'
Γ ⊢ open t2 t : τ2 subst.
Γ: ctx
t2: term
τ1, τ2, τ: typ
t: term
J1: Γ ⊢ (λ) τ t : τ1 ⟹ τ2
J2: Γ ⊢ t2 : τ1
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Γ ⊢ open t2 t : τ2
      apply inversion21 in J1.
Γ: ctx
t2: term
τ1, τ2, τ: typ
t: term
J1: exists C : typ,
  τ1 ⟹ τ2 = τ ⟹ C /\
  (exists L : AtomSet.t,
     forall x,
     x `notin` L -> Γ ++ x ~ τ ⊢ open x t : C)
J2: Γ ⊢ t2 : τ1
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Γ ⊢ open t2 t : τ2
      destruct J1 as [C [hyp1 [L hyp2]]].
Γ: ctx
t2: term
τ1, τ2, τ: typ
t: term
C: typ
hyp1: τ1 ⟹ τ2 = τ ⟹ C
L: AtomSet.t
hyp2: forall x,
x `notin` L -> Γ ++ x ~ τ ⊢ open x t : C
J2: Γ ⊢ t2 : τ1
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ1 ⟹ τ2
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ1
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Γ ⊢ open t2 t : τ2
      inversion hyp1; subst.
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
hyp2: forall x,
x `notin` L -> Γ ++ x ~ τ ⊢ open x t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Γ ⊢ open t2 t : C
      specialize_freshly hyp2.
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
Γ ⊢ open t2 t : C
      rewrite (open_spec _ _ e).
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
Γ ⊢ subst e t2 (open (ret e) t) : C
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
e `notin` FV t
      {
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
Γ ⊢ subst e t2 (open (ret e) t) : C eauto using substitution_r. }
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
e `notin` FV t
      {
Γ: ctx
t2: term
τ: typ
t: term
C: typ
hyp1: τ ⟹ C = τ ⟹ C
L: AtomSet.t
e: atom
hyp2: Γ ++ e ~ τ ⊢ open e t : C
IHJ2: forall t', beta_step t2 t' -> Γ ⊢ t' : τ
IHJ1: forall t',
beta_step ((λ) τ t) t' -> Γ ⊢ t' : τ ⟹ C
J2: Γ ⊢ t2 : τ
Hstep: beta_step (⟨ (λ) τ t ⟩ (t2)) (open t2 t)
Hfresh: e `notin` (L ∪ (FV t2 ∪ (FV t ∪ domset Γ)))
e `notin` FV t fsetdec. }
Qed.

Theorem progress: forall (t: term) τ1,
    nil ⊢ t: τ1 -> value t \/ (exists t', beta_step t t').
forall t τ1,
[] ⊢ t : τ1 -> value t \/ (exists t', beta_step t t')
Proof.
forall t τ1,
[] ⊢ t : τ1 -> value t \/ (exists t', beta_step t t')
  introv J.
t: term
τ1: typ
J: [] ⊢ t : τ1
value t \/ (exists t', beta_step t t') remember [] as ctx.
t: term
τ1: typ
ctx: list (atom * typ)
Heqctx: ctx = []
J: ctx ⊢ t : τ1
value t \/ (exists t', beta_step t t')
  typing_induction; subst.
x: atom
τ: typ
Hin: (x, τ) ∈ []
Huniq: uniq []
value x \/ (exists t', beta_step x t')
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) \/
(exists t', beta_step ((λ) τ0 body) t')
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: [] = [] ->
value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
  -
x: atom
τ: typ
Hin: (x, τ) ∈ []
Huniq: uniq []
value x \/ (exists t', beta_step x t') inversion Hin.
  -
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) \/
(exists t', beta_step ((λ) τ0 body) t') left.
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) constructor.
  -
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: [] = [] ->
value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') specialize (IHJ1 eq_refl).
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    specialize (IHJ2 eq_refl).
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
IHJ1: value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    destruct IHJ1.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    +
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') right.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t' inversion H; subst.
t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
X: typ
t: term
H: value ((λ) X t)
J2: [] ⊢ t2 : τ0
J1: [] ⊢ (λ) X t : τ0 ⟹ τ2
exists t', beta_step (⟨ (λ) X t ⟩ (t2)) t'
      exists (t '(t2)).
t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
X: typ
t: term
H: value ((λ) X t)
J2: [] ⊢ t2 : τ0
J1: [] ⊢ (λ) X t : τ0 ⟹ τ2
beta_step (⟨ (λ) X t ⟩ (t2)) (open t2 t) constructor.
    +
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') right.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t'
      destruct H as [t1' Hstep'].
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
t1': term
Hstep': beta_step t1 t1'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t'
      eauto using beta_app_l.
Qed.

Theorem soundness: forall (t: term) τ1,
    nil ⊢ t: τ1 -> value t \/ (exists t', beta_step t t').
forall t τ1,
[] ⊢ t : τ1 -> value t \/ (exists t', beta_step t t')
Proof.
forall t τ1,
[] ⊢ t : τ1 -> value t \/ (exists t', beta_step t t')
  introv J.
t: term
τ1: typ
J: [] ⊢ t : τ1
value t \/ (exists t', beta_step t t') remember [] as ctx.
t: term
τ1: typ
ctx: list (atom * typ)
Heqctx: ctx = []
J: ctx ⊢ t : τ1
value t \/ (exists t', beta_step t t')
  typing_induction; subst.
x: atom
τ: typ
Hin: (x, τ) ∈ []
Huniq: uniq []
value x \/ (exists t', beta_step x t')
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) \/
(exists t', beta_step ((λ) τ0 body) t')
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: [] = [] ->
value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
  -
x: atom
τ: typ
Hin: (x, τ) ∈ []
Huniq: uniq []
value x \/ (exists t', beta_step x t') inversion Hin.
  -
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) \/
(exists t', beta_step ((λ) τ0 body) t') left.
L: AtomSet.t
τ0, τ2: typ
body: term
IHbody: forall x,
x `notin` L ->
[] ++ x ~ τ0 = [] ->
value (open x body) \/
(exists t', beta_step (open x body) t')
Jbody: forall x,
x `notin` L -> [] ++ x ~ τ0 ⊢ open x body : τ2
value ((λ) τ0 body) constructor.
  -
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: [] = [] ->
value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') specialize (IHJ1 eq_refl).
t1, t2: term
τ0, τ2: typ
IHJ2: [] = [] ->
value t2 \/ (exists t', beta_step t2 t')
IHJ1: value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    specialize (IHJ2 eq_refl).
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
IHJ1: value t1 \/ (exists t', beta_step t1 t')
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    destruct IHJ1.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t')
    +
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') right.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: value t1
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t' inversion H; subst.
t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
X: typ
t: term
H: value ((λ) X t)
J2: [] ⊢ t2 : τ0
J1: [] ⊢ (λ) X t : τ0 ⟹ τ2
exists t', beta_step (⟨ (λ) X t ⟩ (t2)) t'
      exists (t '(t2)).
t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
X: typ
t: term
H: value ((λ) X t)
J2: [] ⊢ t2 : τ0
J1: [] ⊢ (λ) X t : τ0 ⟹ τ2
beta_step (⟨ (λ) X t ⟩ (t2)) (open t2 t) constructor.
    +
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
value (⟨ t1 ⟩ (t2)) \/
(exists t', beta_step (⟨ t1 ⟩ (t2)) t') right.
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
H: exists t', beta_step t1 t'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t'
      destruct H as [t1' Hstep'].
t1, t2: term
τ0, τ2: typ
IHJ2: value t2 \/ (exists t', beta_step t2 t')
t1': term
Hstep': beta_step t1 t1'
J2: [] ⊢ t2 : τ0
J1: [] ⊢ t1 : τ0 ⟹ τ2
exists t', beta_step (⟨ t1 ⟩ (t2)) t'
      eauto using beta_app_l.
Qed.