simp [Pure.pure, StateT.pure]
α ν : 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)ᶜ ⇨ ⊤
no goals