Theorem: LN.free_var_list_to_string_list (FOL/LN/Paper.lean)

State before:
vs : List Var
h1 : ∀ v ∈ vs, Var.lc_at 0 v
⊢ ∃ xs, vs = List.map free_ xs
Tactic:
induction vs
State after:
case nil
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs

case cons
head✝ : Var
tail✝ : List Var
tail_ih✝ : (∀ v ∈ tail✝, Var.lc_at 0 v) → ∃ xs, tail✝ = List.map free_ xs
h1 : ∀ v ∈ head✝ :: tail✝, Var.lc_at 0 v
⊢ ∃ xs, head✝ :: tail✝ = List.map free_ xs

State before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs
Tactic:
case nil =>
  apply Exists.intro []
  simp
State after:
no goals

State before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : ∀ v ∈ hd :: tl, Var.lc_at 0 v
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
case cons hd tl ih =>
  simp at h1
  cases h1
  case intro h1_left h1_right =>
    specialize ih h1_right
    apply Exists.elim ih
    intro xs a1
    cases hd
    case free_ x =>
      apply Exists.intro (x :: xs)
      simp
      exact a1
    case bound_ i =>
      simp only [Var.lc_at] at h1_left
      simp at h1_left
State after:
no goals

State before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ ∃ xs, [] = List.map free_ xs
Tactic:
apply Exists.intro []
State after:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ [] = List.map free_ []

State before:
h1 : ∀ v ∈ [], Var.lc_at 0 v
⊢ [] = List.map free_ []
Tactic:
simp
State after:
no goals

State before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : ∀ v ∈ hd :: tl, Var.lc_at 0 v
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
simp at h1
State after:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : Var.lc_at 0 hd ∧ ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs

State before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : Var.lc_at 0 hd ∧ ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
cases h1
State after:
case intro
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
left✝ : Var.lc_at 0 hd
right✝ : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs

State before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
case intro h1_left h1_right =>
  specialize ih h1_right
  apply Exists.elim ih
  intro xs a1
  cases hd
  case free_ x =>
    apply Exists.intro (x :: xs)
    simp
    exact a1
  case bound_ i =>
    simp only [Var.lc_at] at h1_left
    simp at h1_left
State after:
no goals

State before:
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
specialize ih h1_right
State after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs

State before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
apply Exists.elim ih
State after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∀ (a : List String), tl = List.map free_ a → ∃ xs, hd :: tl = List.map free_ xs

State before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
⊢ ∀ (a : List String), tl = List.map free_ a → ∃ xs, hd :: tl = List.map free_ xs
Tactic:
intro xs a1
State after:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs

State before:
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
⊢ ∃ xs, hd :: tl = List.map free_ xs
Tactic:
cases hd
State after:
case free_
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
a✝ : String
h1_left : Var.lc_at 0 (free_ a✝)
⊢ ∃ xs, free_ a✝ :: tl = List.map free_ xs

case bound_
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
a✝ : ℕ
h1_left : Var.lc_at 0 (bound_ a✝)
⊢ ∃ xs, bound_ a✝ :: tl = List.map free_ xs

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ ∃ xs, free_ x :: tl = List.map free_ xs
Tactic:
case free_ x =>
  apply Exists.intro (x :: xs)
  simp
  exact a1
State after:
no goals

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : Var.lc_at 0 (bound_ i)
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
case bound_ i =>
  simp only [Var.lc_at] at h1_left
  simp at h1_left
State after:
no goals

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ ∃ xs, free_ x :: tl = List.map free_ xs
Tactic:
apply Exists.intro (x :: xs)
State after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ free_ x :: tl = List.map free_ (x :: xs)

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ free_ x :: tl = List.map free_ (x :: xs)
Tactic:
simp
State after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ tl = List.map free_ xs

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ tl = List.map free_ xs
Tactic:
exact a1
State after:
no goals

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : Var.lc_at 0 (bound_ i)
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
simp only [Var.lc_at] at h1_left
State after:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : i < 0
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs

State before:
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : i < 0
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
Tactic:
simp at h1_left
State after:
no goals