proposition: Lemma rule_elimination : forall rp : Reduction_pair Sig, compat (rp_succ_eq rp) Rge -> compat (rp_succ rp ) Rgt -> WF (red Rge) -> WF (red (Rgt ++ Rge)).
proof: Proof. Proof with auto. intros. eapply WF_incl. apply red_incl_red_mod. change (nil (A:=rule)) with (nil (A:=rule) ++ nil). apply rule_elimination_mod with rp... apply compat_empty. apply compat_empty. apply WF_incl with (red Rge)... apply red_mod_empty_incl_red. Qed.
imports: CoLoR(ATrs SN ARelation RelUtil ACompat LogicUtil) Coq(List)