proposition: Lemma case_inr' {a b c d} (ac : C a c) (bc : C b c) (cd : C c d) : inr_ >>> (case_ ac bc >>> cd) ⩯ bc >>> cd.
proof: Proof. rewrite <- cat_assoc, case_inr; reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)