no goals
J : Type w
C : Type u
inst✝¹ : Category C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ ι s = l ≫ ι s
⊢ k ≫ s.π.app one = l ≫ s.π.app one
rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]