intro hP hQ s
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
⊢ encodesProp e1 P → (∀ (s : LawfulState ν), encodesProp (f (↑e1 s).1) Q) → encodesProp (e1 >>= f) (P ⊓ Q)
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
hP : encodesProp e1 P
hQ : ∀ (s : LawfulState ν), encodesProp (f (↑e1 s).1) Q
s : LawfulState ν
⊢ let s' := (↑(e1 >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q