proposition: Lemma rule_elimination_hd_red : forall wp : Weak_reduction_pair Sig, compat (wp_succ_eq wp) Rge -> compat (wp_succ wp ) Rgt -> WF (hd_red Rge) -> WF (hd_red (Rgt ++ Rge)).
proof: Proof. Proof with auto. intros. eapply WF_incl. apply hd_red_incl_hd_red_mod. apply rule_elimination_hd_mod with wp... apply compat_empty. apply WF_incl with (hd_red Rge)... apply hd_red_mod_empty_incl_hd_red. Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)