proposition: Lemma loop_vanishing_1 {a b} (f : C (bif i a) (bif i b)) : loop f ⩯ unit_l' >>> f >>> unit_l.
proof: Proof. unfold loop. rewrite iter_unfold. cat_auto. cat_auto_step. cat_auto. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)