proposition: Lemma manna_ness (R : rules) succ : reduction_ordering succ -> compat succ R -> WF (red R).
proof: Proof. intros. destruct H. apply (WF_incl succ). apply compat_red; auto. hyp. Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)