∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements),
  (CategoryTheory.ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst)) (M.freeYonedaCoproductMk m) = m.snd