proposition: Lemma manna_ness_hd_mod (R E : rules) (wp : Weak_reduction_pair Sig) : compat (wp_succ_eq wp) E -> compat (wp_succ wp) R -> WF (hd_red_mod E R).
proof: Proof. intros. apply (WF_incl (wp_succ wp)). destruct wp; simpl in *. apply compat_hd_red_mod with wp_succ_eq; try split; hyp. destruct wp; hyp. Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)