replace hQ := hQ s'
case 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✝ }
hQ :
  ∀ (s : LawfulState ν),
    (↑{ val := e2, property := he2✝ } s).2.vMap = s.vMap ∧
      (↑{ val := e2, property := he2✝ } s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑{ val := e2, property := he2✝ } s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
case 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✝ }
hQ :
  (↑{ val := e2, property := he2✝ } s').2.vMap = s'.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)