proposition: Lemma term_neq_type : forall M N, type M <> type N -> M <> N.
proof: Proof. intros; intro MN. absurd (type M = type N); trivial. rewrite MN; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)