proposition: Lemma list_permut_acc : forall R l1 l2, permut l2 l1 -> Acc (multiset_extension_step R) l1 -> Acc (multiset_extension_step R) l2.
proof: Proof. intros R l1 l2 Meq A1; apply Acc_intro; intros l M2; inversion A1; apply H; subst. apply list_permut_multiset_extension_step_2 with l2; assumption. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)