proposition: Lemma context_multiset_extension_step_app1 : forall R l1 l2 l, multiset_extension_step R l1 l2 -> multiset_extension_step R (l ++ l1) (l ++ l2).
proof: Proof. intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2]. apply (@rmv_case R (l++l1) (l++l2) (l++l12) la a); trivial. apply permut_trans with (l ++ la ++ l12). rewrite <- permut_app1; trivial. do 2 rewrite <- app_ass; rewrite <- permut_app2; trivial. apply list_permut_app_app. apply permut_trans with (l ++ a :: l12). rewrite <- permut_app1; trivial. apply permut_sym; rewrite <- permut_cons_inside. apply permut_refl. apply (equiv_refl _ _ eq_proof). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)