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))