proposition: Lemma WF_red_empty : WF (red (@nil rule)).
proof: Proof. intro x. apply SN_intro. intros y Exy. redtac. contr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)