scheme :: MODELC_2:sch 2
LTLCompInd{ P1[ LTL-formula] } :
for H being LTL-formula holds P1[H]
provided
A1: for H being LTL-formula st ( for F being LTL-formula st F is_proper_subformula_of H holds
P1[F] ) holds
P1[H]