proposition: Lemma HAccTermsToTermlist : forall ss, (forall s, In s ss -> Acc (transp r) s) -> Acc mult ss.
proof: Proof. intros ss Hsub; cut (Acc (MultisetLT r) (list2multiset ss)). unfold mult; apply (Acc_inverse_image (list A) Multiset (MultisetLT r) list2multiset ss). cut (Acc (MultisetLt r) (list2multiset ss)). apply Inclusion.Acc_incl; intros M N; unfold MultisetLT, MultisetLt, transp; simpl; apply direct_subset_red; trivial. apply r_eqA. apply mord_acc with (gtA := r) (M := list2multiset ss); trivial. apply r_eqA. intros x Hx; apply (Hsub x). elim (member_multiset_list ss Hx). apply In_eqA_compat. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)