proposition: Lemma HAccTermlistToTerms : transitive r -> forall ss : list A, Acc mult ss -> (forall s, In s ss -> Acc (transp r) s).
proof: Proof. intros r_trans ss acc_ss. intros s s_in_ss; apply acc_mord with (gtA := r) (M := list2multiset ss); try hyp. apply r_eqA. apply Acc_list_multiset; trivial. gen s_in_ss; apply member_list_multiset. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)