theorem Th32: :: MODELC_2:32

for F, H being LTL-formula st H is_proper_subformula_of F holds
len H < len F