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

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