∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt)
  (fac :
    ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i)
  (uniq :
    ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt),
      (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E)
  (E : CategoryTheory.Limits.Multifork I), (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E