+/*
+l :: (Step pre inter)
+| E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
+bm2 :: BM (Step pre inter)
+| E.e: OWait (BM (Step inter post) (Step post post)) (SBM inter post)
+
+need:
+:: BM (Step pre inter) (Step pre post)
+*/
+opti (OSeq bm1 l (OWait bm2 sbm)) = bm.f2 (opti (sbm.st2 l))