proposition: Lemma pair_cat {a b c d} (ab : C a b) (bc : C b c) (bd : C b d) : (ab >>> pair_ bc bd ⩯ pair_ (ab >>> bc) (ab >>> bd)).
proof: Proof. apply pair_universal. - rewrite pair_fst'; reflexivity. - rewrite pair_snd'; reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)