proposition: Lemma bimap_sub_unfold a b c d (f : sub a c) (g : sub b d) : eq2 (C := C) (bimap (C := sub) f g) (to_bif >>> bimap (C := C) f g >>> from_bif).
proof: Proof. unfold bimap at 1, Bimap_Coproduct at 1. unfold_sub. rewrite <- 2 cat_assoc. rewrite <- cat_case. rewrite cat_assoc. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Category CategoryFunctor)