push_neg at h
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬∃ o, Object rtr cpt i o
⊢ False
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∀ (o : Component.type α cpt), ¬Object rtr cpt i o
⊢ False