for F, H being LTL-formula st H is neg-inner-most & F is_subformula_of H holds
F is neg-inner-most by MODELC_2:35;