proposition: Lemma loop_natural_right {a b b' c} (f : C (bif c a) (bif c b)) (g : C b b') : loop f >>> g ⩯ loop (f >>> bimap (id_ _) g).
proof: Proof. unfold loop. rewrite cat_assoc. cat_auto_step. rewrite iter_natural. cat_auto_step. rewrite !cat_assoc, !bimap_cat, !cat_id_l, !cat_id_r. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)