let rec until is_strong a b = if is_strong then Until (a, b) else or_ (until true a b) (always a) and eventually a = until true True a and always a = not_ (eventually (not_ a))