Theorem: LeanSAT.Encode.EncCNF.LawfulState.assumeVars_withTemps (LeanSAT/Encode/EncCNF.lean)

State before:
ν : Type u_1
n : ℕ
s : LawfulState ν
⊢ (withTemps s).assumeVars = Clause.map (Literal (ν ⊕ Fin n)) Sum.inl s.assumeVars
Tactic:
simp [LawfulState.withTemps, State.withTemps]
State after:
no goals