∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  (X : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)),
  ((CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt