proposition: Corollary unit_l_mono {UnitLIso_C : UnitLIso} : forall a, unit_l >>> unit_l' ⩯ id_ (bif i a).
proof: Proof. intros; apply semi_iso, UnitLIso_C. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryFunctor)