replace hQ := hQ s
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= 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
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= 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