no goals
C : Type u
inst✝ : Category C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ ι K (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
    ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]