proposition: Lemma bimap_slide {a b c d} (ac: C a c) (bd: C b d) : bimap ac bd ⩯ bimap ac (id_ _) >>> bimap (id_ _) bd.
proof: Proof. rewrite bimap_cat, cat_id_l, cat_id_r. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)