induction A with
| var s =>
  rw [eval]
  rw [Occurs] at h
  rw [if_neg h, eval]
| tr =>
  rw [eval, eval]
| fls =>
  rw [eval, eval]
| neg A ihA =>
  rw [eval, eval]
  rw [Occurs] at h
  rw [ihA h]
| conj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| disj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| impl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| biImpl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
h : ¬Occurs v A
b : Bool
⊢ eval (fun w => if v = w then b else τ w) A = eval τ A
no goals