let rec next_ae is_strong is_forall n0 n1 a =
  if n0 > n1 then raise (Invalid_argument "Ltl.next_ae: First count is greater than second.");
  if n0 = n1 then
    next_repeat is_strong n0 a
  else
    (if is_forall then and_ else or_) (next_repeat is_strong n0 a) (next_ae is_strong is_forall (n0 + 1) n1 a)