proposition: Lemma red_mod0_incl_red_mod : forall E R, red_mod0 E R << red_mod E R.
proof: Proof. intros E R t u. unfold red_mod0. tauto. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)