proposition: Lemma remove_context_multiset_extension_step_app1 : forall R, (forall a, ~R a a) -> forall l1 l2 l, multiset_extension_step R (l ++ l1) (l ++ l2) -> multiset_extension_step R l1 l2.
proof: Proof. intros R irrefl_R l1 l2 l; generalize l1 l2; clear l1 l2; induction l as [ | a l]; trivial. intros l1 l2 H; assert (H' : multiset_extension_step R (a :: l1) (a :: l2)). apply IHl. apply list_permut_multiset_extension_step_2 with ((a :: l) ++ l2). simpl; rewrite <- permut_cons_inside; auto. apply (equiv_refl _ _ eq_proof). apply list_permut_multiset_extension_step_1 with ((a :: l) ++ l1); trivial. simpl; rewrite <- permut_cons_inside; auto. apply (equiv_refl _ _ eq_proof). apply context_multiset_extension_step_cons with a; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)