proposition: Lemma WF_red : WF (red R) <-> WF (Srs.red (srs_of_trs R)).
proof: Proof. rewrite <- red_mod_empty, <- Srs.red_mod_empty. apply WF_red_mod. unfold rules_preserve_vars. simpl. tauto. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)