generalize hs' : e1 s = s' at *
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
hP :
  (e1 s).2.vMap = s.vMap ∧
    (e1 s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
he1 : s.nextVar ≤ (e1 s).2.nextVar
⊢ (match e1 s with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match e1 s with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match e1 s with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
s' : Id (α × LawfulState ν)
hs' : e1 s = s'
hP :
  s'.2.vMap = s.vMap ∧
    s'.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f s'.1) s).2.vMap = s.vMap ∧
      (↑(f s'.1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f s'.1) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.2.nextVar
⊢ (match s' with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match s' with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match s' with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)