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

State before:
ν : Type u_1
n : ℕ
vm : ν → IVar
av : Array (Literal ν)
s : State (ν ⊕ Fin n)
⊢ (withoutTemps vm av s).assumeVars = av
Tactic:
simp [State.withoutTemps]
State after:
no goals