Theorem: LN.IsFreeIffExistsString (FOL/LN/Binders.lean)

State before:
v : Var
⊢ v.isFree ↔ ∃ x, v = free_ x
Tactic:
cases v
State after:
case free_
a✝ : String
⊢ (free_ a✝).isFree ↔ ∃ x, free_ a✝ = free_ x

case bound_
a✝ : ℕ
⊢ (bound_ a✝).isFree ↔ ∃ x, bound_ a✝ = free_ x

State before:
x : String
⊢ (free_ x).isFree ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
case free_ x =>
  simp only [isFree]
  simp
State after:
no goals

State before:
i : ℕ
⊢ (bound_ i).isFree ↔ ∃ x, bound_ i = free_ x
Tactic:
case bound_ i =>
  simp only [isFree]
  simp
State after:
no goals

State before:
x : String
⊢ (free_ x).isFree ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
simp only [isFree]
State after:
x : String
⊢ True ↔ ∃ x_1, free_ x = free_ x_1

State before:
x : String
⊢ True ↔ ∃ x_1, free_ x = free_ x_1
Tactic:
simp
State after:
no goals

State before:
i : ℕ
⊢ (bound_ i).isFree ↔ ∃ x, bound_ i = free_ x
Tactic:
simp only [isFree]
State after:
i : ℕ
⊢ False ↔ ∃ x, False

State before:
i : ℕ
⊢ False ↔ ∃ x, False
Tactic:
simp
State after:
no goals