∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (e e_1 : x.fst ≅ y.fst) (e_e : e = e_1) (he : F.map e.hom x.snd = y.snd),
  CategoryTheory.CategoryOfElements.isoMk x y e he = CategoryTheory.CategoryOfElements.isoMk x y e_1 ⋯