induction d <;> try exact Partial.mem_iff.mpr ⟨_, obj?_some_extend ‹_› ‹_›⟩
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
d : rcn₁ <[rtr] rcn₂
⊢ rcn₁ ∈ rtr[Component.rcn]
case depOverlap
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
a✝⁴ : rtr[Component.rcn][i₁✝] = some rcn₁✝
a✝³ : rtr[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ ∈ rtr[Component.rcn]

case trans
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr] i₂✝
a✝ : i₂✝ <[rtr] i₃✝
a_ih✝¹ : i₁✝ ∈ rtr[Component.rcn]
a_ih✝ : i₂✝ ∈ rtr[Component.rcn]
⊢ i₁✝ ∈ rtr[Component.rcn]