theorem Th6: :: LTLAXIO2:6

for f being FinSequence of LTLB_WFF st len f > 0 holds
(con f) /. 1 = f /. 1