proposition: Lemma pair_split {a b c} (f g : C a (bif b c)) : (f >>> fst_ ⩯ g >>> fst_) -> (f >>> snd_ ⩯ g >>> snd_) -> f ⩯ g.
proof: Proof. intros. rewrite (pair_eta' g). apply pair_universal; assumption. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)