Theorem: Reactor.StrictMember.unique (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
s₁ s₂ : StrictMember cpt i rtr
⊢ s₁ = s₂
Tactic:
injection unique_ids.allEq (.strict s₁) (.strict s₂)
State after:
no goals