∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) =
    CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (CategoryTheory.CategoryStruct.comp (I.snd i) h)