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