Theorem: Partial.const_ids (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
as : Set α
b : β
⊢ ids (const as b) = as
Tactic:
simp [const, ids]
State after:
no goals