proposition: Lemma loop_natural_left {a a' b c} (f : C (bif c a) (bif c b)) (g : C a' a) : g >>> loop f ⩯ loop (bimap (id_ _) g >>> f).
proof: Proof. unfold loop. transitivity (inr_ >>> iter (bimap (id_ c) g >>> inl_ >>> case_ (f >>> bimap inl_ (id_ b)) inr_)). - rewrite iter_dinatural. cat_auto. do 2 cat_auto_step. cat_auto. - cat_auto. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)