exact ho _ ⟨.final $ Option.ne_none_iff_exists.mp h |>.choose_spec.symm⟩
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
h : ¬rtr{cpt}{i} = none
⊢ False
no goals