proposition: Lemma manna_ness_mod (R E : rules) (rp : Reduction_pair Sig) : compat (rp_succ_eq rp) E -> compat (rp_succ rp) R -> WF (red_mod E R).
proof: Proof. intros. apply (WF_incl (rp_succ rp)). destruct rp; simpl in *. apply compat_red_mod with rp_succ_eq; try split; hyp. destruct rp; hyp. Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)