for k being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)