exact ⟨_, obj?_some_nested h ho⟩
case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
no goals