proposition: Lemma rule_elimination_hd_mod : forall wp : Weak_reduction_pair Sig, compat (wp_succ_eq wp) E -> compat (wp_succ_eq wp) Rge -> compat (wp_succ wp ) Rgt -> WF (hd_red_mod E Rge) -> WF (hd_red_mod E (Rgt ++ Rge)).
proof: Proof. Proof with auto. intros. apply WF_incl with (red E # @ (hd_red Rgt U hd_red Rge)). comp. apply hd_red_union. apply wf_rel_mod_simpl... apply WF_incl with (hd_red_mod (Rge ++ E) Rgt). comp. apply rtc_incl. incl_trans (red Rge U red E). union. apply hd_red_incl_red. apply red_union_inv. apply manna_ness_hd_mod with wp... apply compat_app... Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)