proposition: Lemma WF_red_flat : WF (red R) <-> WF (red flat_rules).
proof: Proof. eapply WF_red_flat. apply arity_some_symbol. apply Fs_ok. apply Nat.le_refl. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)