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

State before:
α ν : Type u_1
a : α
⊢ encodesProp (pure a) ⊤
Tactic:
intro s
State after:
α ν : Type u_1
a : α
s : LawfulState ν
⊢ let s' := (↑(pure a) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ ⊤

State before:
α ν : Type u_1
a : α
s : LawfulState ν
⊢ let s' := (↑(pure a) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ ⊤
Tactic:
simp [Pure.pure, StateT.pure]
State after:
no goals