∀ {V W : Type u_2} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W]
  (e : CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W),
  (∀ (X : V), e.hom.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (e.hom.obj X)) →
    ∀ (Y : ↑(CategoryTheory.ReflQuiv.of W)),
      (CategoryTheory.Quiv.homEquivOfIso e) (e.inv.map (CategoryTheory.ReflQuiver.id Y)) =
        (CategoryTheory.Quiv.homEquivOfIso e) (CategoryTheory.ReflQuiver.id (e.inv.obj Y))