proposition: Lemma context_multiset_extension_step_app2 : forall R l1 l2 l, multiset_extension_step R l1 l2 -> multiset_extension_step R (l1 ++ l) (l2 ++ l).
proof: Proof. intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2]. apply (@rmv_case R (l1++l) (l2++l) (l12++l) la a); trivial. rewrite <- app_ass; rewrite <- permut_app2; trivial. rewrite app_comm_cons; rewrite <- permut_app2; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)