proposition: Lemma swap_case (a b c: obj) (f: C a c) (g: C b c) : swap >>> case_ f g ⩯ case_ g f.
proof: Proof. intros; unfold swap, Swap_Coproduct. rewrite cat_case, inr_case, inl_case. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)