proposition: Lemma red_empty : forall t u : term, red nil # t u -> t = u.
proof: Proof. intros. induction H. redtac. contr. refl. congruence. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)