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