proposition: Lemma tau_dec : forall f R ts ss, (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) -> {tau f R ts ss} + {~tau f R ts ss}.
proof: Proof. intros. unfold tau, mytau. destruct (status_dec f); rewrite e. apply lex_status_dec. hyp. apply mul_status_dec. hyp. Defined.
imports: CoLoR(VPrecedence MultisetListOrder ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations)