Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp (LeanSAT/Encode/VEncCNF.lean)

State before:
ν α β : 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)
Tactic:
intro hP hQ s
State after:
ν α β : 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

State before:
ν α β : 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
Tactic:
simp [encodesProp, encodesProp.aux] at hP hQ
State after:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
s : LawfulState ν
hP :
  ∀ (s : LawfulState ν),
    (↑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 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 τ)
⊢ 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

State before:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
s : LawfulState ν
hP :
  ∀ (s : LawfulState ν),
    (↑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 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 τ)
⊢ 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
Tactic:
rcases e1 with ⟨e1,he1⟩
State after:
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 :
  ∀ (s : LawfulState ν),
    (↑{ 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 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

State before:
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 :
  ∀ (s : LawfulState ν),
    (↑{ 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 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
Tactic:
replace hP := hP s
State after:
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

State before:
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
Tactic:
replace hQ := hQ s
State after:
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

State before:
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
Tactic:
simp [Bind.bind, StateT.bind] at hP hQ ⊢
State after:
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 :
  (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 τ)
⊢ (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 τ)

State before:
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 :
  (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 τ)
⊢ (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 τ)
Tactic:
replace he1 := he1 s
State after:
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 τ)

State before:
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 τ)
Tactic:
generalize hs' : e1 s = s' at *
State after:
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 τ)

State before:
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 τ)
Tactic:
rcases s' with ⟨a,s'⟩
State after:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  (a, s').2.vMap = s.vMap ∧
    (a, s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (a, s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f (a, s').1) s).2.vMap = s.vMap ∧
      (↑(f (a, s').1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (a, s').1) s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ (a, s').2.nextVar
⊢ (match (a, s') with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match (a, s') with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match (a, s') with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  (a, s').2.vMap = s.vMap ∧
    (a, s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (a, s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f (a, s').1) s).2.vMap = s.vMap ∧
      (↑(f (a, s').1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (a, s').1) s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ (a, s').2.nextVar
⊢ (match (a, s') with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match (a, s') with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match (a, s') with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
simp at *
State after:
case 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 τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f a) s).2.vMap = s.vMap ∧
      (↑(f a) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f a) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.nextVar
⊢ (↑(f a) s').2.vMap = s.vMap ∧
    (↑(f a) s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑(f a) s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
case 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 τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f a) s).2.vMap = s.vMap ∧
      (↑(f a) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f a) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.nextVar
⊢ (↑(f a) s').2.vMap = s.vMap ∧
    (↑(f a) s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑(f a) s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
generalize he2 : (f a) = e2 at *
State after:
case 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 : EncCNF ν β
he2 : f a = e2
hQ :
  ∀ (s : LawfulState ν),
    (↑e2 s).2.vMap = s.vMap ∧
      (↑e2 s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑e2 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑e2 s').2.vMap = s.vMap ∧
    (↑e2 s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑e2 s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
case 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 : EncCNF ν β
he2 : f a = e2
hQ :
  ∀ (s : LawfulState ν),
    (↑e2 s).2.vMap = s.vMap ∧
      (↑e2 s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑e2 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑e2 s').2.vMap = s.vMap ∧
    (↑e2 s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑e2 s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
rcases e2 with ⟨e2,he2⟩
State after:
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 τ)

State before:
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 τ)
Tactic:
replace hQ := hQ s'
State after:
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 τ)

State before:
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 τ)
Tactic:
simp at *
State after:
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 :
  (e2 s').2.vMap = s'.vMap ∧
    (e2 s').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e2 s').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (e2 s').2.vMap = s.vMap ∧
    (e2 s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e2 s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
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 :
  (e2 s').2.vMap = s'.vMap ∧
    (e2 s').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e2 s').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (e2 s').2.vMap = s.vMap ∧
    (e2 s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e2 s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
generalize hs'' : e2 s' = s'' at *
State after:
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✝ }
s'' : Id (β × LawfulState ν)
hs'' : e2 s' = s''
hQ :
  s''.2.vMap = s'.vMap ∧
    s''.2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.2.vMap = s.vMap ∧
    s''.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
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✝ }
s'' : Id (β × LawfulState ν)
hs'' : e2 s' = s''
hQ :
  s''.2.vMap = s'.vMap ∧
    s''.2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.2.vMap = s.vMap ∧
    s''.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
rcases s'' with ⟨b,s''⟩
State after:
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 τ)

State before:
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 τ)
Tactic:
open PropPred in simp at hP hQ ⊢
aesop
State after:
no goals

State before:
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 τ)
Tactic:
simp at hP hQ ⊢
State after:
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 :
  s''.vMap = s'.vMap ∧
    s''.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.vMap = s.vMap ∧
    s''.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)

State before:
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 :
  s''.vMap = s'.vMap ∧
    s''.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.vMap = s.vMap ∧
    s''.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
aesop
State after:
no goals