for F, H being LTL-formula st F is next holds
( H is_immediate_constituent_of F iff H = the_argument_of F )