proposition: Lemma mul_status_dec : (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) -> {mult (transp R) ts ss} + {~mult (transp R) ts ss}.
proof: Proof. intros. assert (eq_comp : Proper (eq ==> eq ==> impl) (transp R)). intros a b ab c d cd. subst. fo. destruct (@mOrd_dec_aux (transp R) eq_comp (list2multiset ss) (list2multiset ts)). assert (R_transp_dec : forall t s, In t ts -> In s ss -> {(transp R) s t} + {~(transp R) s t}). intros. destruct (X t s); intuition. intros. apply R_transp_dec. destruct (member_multiset_list ts H0). compute in H2. rewrite H2. hyp. destruct (member_multiset_list ss H). compute in H2. rewrite H2. hyp. intuition. intuition. Defined.
imports: CoLoR(VPrecedence ListUtil VTerm RelMidex LogicUtil AccUtil) Coq(Relations Morphisms Basics)