proposition: Lemma WF_red_mod_flat : WF (red_mod E R) <-> WF (red_mod (flat_mod_rules E) (flat_mod_rules R)).
proof: Proof. eapply WF_red_mod_flat. apply arity_some_symbol. apply Fs_ok. apply Nat.le_max_l. apply Nat.le_max_r. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)