theorem :: LTLAXIO2:29

for f being FinSequence of LTLB_WFF
for k being Nat st k in dom f holds
(f /. k) => ('not' ((con (nega f)) /. (len (con (nega f))))) is ctaut