for v being LTL-formula
for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds
len N2 <= (len N1) - 1