proposition: Lemma ma_termination : let R_gt := partition part_succ R in let R_ge := partition part_succeq R in monotone I succ -> snd R_ge = nil -> WF (red (snd R_gt)) -> WF (red R).
proof: Proof. intros. apply WF_incl with (red_mod nil R). apply red_incl_red_mod. apply ma_relative_termination. hyp. hyp. trivial. simpl. apply WF_incl with (red (snd (partition part_succ R))). apply red_mod_empty_incl_red. hyp. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)