simp [satisfies_iff, Array.mem_def, and]
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (and f1 f2) ↔ τ ⊨ toPropFun f1 ⊓ toPropFun f2
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ (∀ (C : Clause L), C ∈ f1.data ∨ C ∈ f2.data → τ ⊨ Clause.toPropFun C) ↔
    (∀ C ∈ f1.data, τ ⊨ Clause.toPropFun C) ∧ ∀ C ∈ f2.data, τ ⊨ Clause.toPropFun C