∀ {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J (Type u_1))
  (s : I.sections),
  (fun i =>
      match i with
      | CategoryTheory.Limits.WalkingMulticospan.left i => s.val i
      | CategoryTheory.Limits.WalkingMulticospan.right j => I.fst j (s.val (J.fst j))) ∈
    I.multicospan.sections