open PropPred in simp at hP hQ ⊢
aesop
case mk.mk.mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
he1 : s.nextVar ≤ s'.nextVar
e2 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  (b, s'').2.vMap = s'.vMap ∧
    (b, s'').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (b, s'').2.vMap = s.vMap ∧
    (b, s'').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
no goals