theorem :: LTLAXIO2:9

for f being FinSequence of LTLB_WFF
for i being Nat st i in dom f holds
(nex f) /. i = 'X' (f /. i)