have ⟨s, hs⟩ := Object.strict_elim $ Object.iff_obj?_some.mpr ho
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
s : StrictMember cpt i' rtr'
hs : StrictMember.object s = o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o