theorem :: LTLAXIO2:30

for f, f1 being FinSequence of LTLB_WFF st rng f c= rng f1 holds
('not' ((con (nega f)) /. (len (con (nega f))))) => ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut