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

State before:
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
⊢ (withoutTemps s vMap vMapLt vMapInj av).assumeVars = av
Tactic:
simp [LawfulState.withoutTemps]
State after:
no goals