∀ {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J (Type u_1))
  (s : ↑I.multicospan.sections),
  (fun s =>
        ⟨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)),
          ⋯⟩)
      ((fun s => { val := fun i => ↑s (CategoryTheory.Limits.WalkingMulticospan.left i), property := ⋯ }) s) =
    s