proposition: Lemma Acc_list_multiset : transitive r -> forall ss, Acc mult ss -> Acc (MultisetLt r) (list2multiset ss).
proof: Proof. intros r_trans ss Hacc. apply (Acc_iso (MultisetLt r) (list2multiset ss) (fun (l : list A) (M : Multiset) => list2multiset l =mul= M) (R := fun ss ts : list A => MultisetLt r (list2multiset ss) (list2multiset ts)) (x := ss)); trivial. intros ts M N Hts HMN. exists (multiset2list M). gen HMN; unfold MultisetLt,transp; simpl. apply MultisetGt_morph. rewrite Hts; auto with multisets. rewrite (double_convertion M); auto with multisets. exact (double_convertion M). auto with multisets. gen Hacc; unfold mult; apply Acc_eq_rel; trivial. intros a b; elim (red_eq_direct r_trans r_eqA (list2multiset b) (list2multiset a)); split; trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)