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