for F, H being LTL-formula st F is_proper_subformula_of 'X' H holds
F is_subformula_of H