proposition: Lemma pair_bimap {a b b' c c'} (fb : C a b) (fc : C a c) (gb : C b b') (gc : C c c') : pair_ fb fc >>> bimap gb gc ⩯ pair_ (fb >>> gb) (fc >>> gc).
proof: Proof. cat_auto_prod'. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)