proposition: Lemma bimap_case {a a' b b' c} (fa : C a a') (fb : C b b') (ga : C a' c) (gb : C b' c) : bimap fa fb >>> case_ ga gb ⩯ case_ (fa >>> ga) (fb >>> gb).
proof: Proof. cat_auto'. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)