theorem :: MODELC_3:67

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & H is neg-inner-most holds
( the_left_argument_of H is neg-inner-most & the_right_argument_of H is neg-inner-most )