exact Equivalent.symm e
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₂
⊢ rtr₂ ≈ rtr₁
no goals