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