∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {val : (i : J.L) → I.left i} {property : ∀ (r : J.R), I.fst r (val (J.fst r)) = I.snd r (val (J.snd r))}
  {val_1 : (i : J.L) → I.left i} {property_1 : ∀ (r : J.R), I.fst r (val_1 (J.fst r)) = I.snd r (val_1 (J.snd r))},
  { val := val, property := property } = { val := val_1, property := property_1 } → val = val_1