proposition: Lemma WF_rp_red : forall R, forallb (brule bsucceq) R = true -> WF (red (filter (brule (neg bsucc)) R)) -> WF (red R).
proof: Proof. intros. rewrite <- red_mod_empty. apply WF_rp_red_mod. refl. hyp. simpl. rewrite red_mod_empty. hyp. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat)