proposition: Lemma list_permut_acc : forall R l1 l2, list_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; setoid_rewrite <- Meq; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut