proposition: Lemma rule_elimination_mod : forall rp : Reduction_pair Sig, compat (rp_succ rp) Rgt -> compat (rp_succ_eq rp) Rge -> compat (rp_succ rp) Egt -> compat (rp_succ_eq rp) Ege -> WF (red_mod Ege Rge) -> WF (red_mod (Egt ++ Ege) (Rgt ++ Rge)).
proof: Proof. Proof with auto. intros. apply WF_incl with ((red Egt U red Ege)# @ (red Rgt U red Rge)). comp. apply rtc_incl. incl_trans (red Egt U red Ege)... apply red_union. apply red_union. apply wf_rel_mod... apply WF_incl with ((red (Rge ++ Ege)# @ (red (Rgt ++ Egt)))). comp. apply rtc_incl. apply red_union_inv. apply red_union_inv. apply manna_ness_mod with rp; apply compat_app... Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)