Theorem: LeanSAT.Encode.EncCNF.State.toPropFun_addClause (LeanSAT/Encode/EncCNF.lean)

State before:
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)
Tactic:
simp [addClause, BooleanAlgebra.himp_eq, sup_comm]
State after:
no goals