proposition: Lemma list_permut_multiset_extension_step_2 : forall R l1 l2 l, list_permut l1 l2 -> multiset_extension_step R l l1 -> multiset_extension_step R l l2.
proof: Proof. intros R l1 l2 l P M1; inversion M1; subst. apply (rmv_case (l1:=l) (l2:=l2) (l:=l4) R la H); trivial; setoid_rewrite <- P; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut