simp [addClause, BooleanAlgebra.himp_eq, sup_comm]
L : Type ?u.1027
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : State ν
⊢ Cnf.toPropFun (addClause C s).cnf =
    Cnf.toPropFun s.cnf ⊓ PropFun.map s.vMap ((Clause.toPropFun s.assumeVars)ᶜ ⇨ Clause.toPropFun C)
no goals