proposition: Lemma status_dec : forall f, {status f = lexicographic} + {status f = multiset}.
proof: Proof. intros. destruct (status f); intuition. Defined.
imports: CoLoR(VPrecedence MultisetListOrder ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations)