simp [or, satisfies_iff]
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) ↔
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l