proposition: Corollary assoc_r_mono {AssocIso_C : AssocIso} : forall a b c, assoc_r >>> assoc_l ⩯ id_ (bif (bif a b) c).
proof: Proof. intros; apply semi_iso, AssocIso_C. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryFunctor)