proposition: Lemma coprod_split {a b c} (f g : C (bif a b) c) : (inl_ >>> f ⩯ inl_ >>> g) -> (inr_ >>> f ⩯ inr_ >>> g) -> f ⩯ g.
proof: Proof. intros. rewrite (case_eta' g). apply case_universal; assumption. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)