∀ {J : CategoryTheory.Limits.MulticospanShape} [inst : DecidableEq J.R] (a b : J.R)
  (x : CategoryTheory.Limits.WalkingMulticospan.right a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b),
  x ∈ if e : a = b then {CategoryTheory.eqToHom ⋯} else ∅