rw [eval, eval]
case fls
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
h : ¬Occurs v fls
⊢ eval (fun w => if v = w then b else τ w) fls = eval τ fls
no goals