proposition: Lemma list_permut_multiset_extension_step_1 : forall R l1 l2 l, permut l1 l2 -> multiset_extension_step R l1 l -> multiset_extension_step R l2 l.
proof: Proof. intros R l1 l2 l P M1; inversion M1 as [ k1 k l1' la a la_R_a P1 P2]; subst. apply (rmv_case (l1:=l2) (l2:=l) (l:=l1') R la la_R_a); trivial. apply permut_trans with l1. apply permut_sym; assumption. assumption. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)