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