proposition: Lemma pair_fst' {a b c d} (ca : C c a) (cb : C c b) (dc : C d c) : dc >>> pair_ ca cb >>> fst_ ⩯ dc >>> ca.
proof: Proof. rewrite cat_assoc, pair_fst. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)