proposition: Lemma remove_context_list_permut_app2 : forall l l1 l2, list_permut (l1 ++ l) (l2 ++ l) -> list_permut l1 l2.
proof: Proof. intros l l1 l2; unfold list_permut, meq; simpl; intros H a; generalize (H a); rewrite (multiplicity_app l1 l); rewrite (multiplicity_app l2 l); intros; apply Nat.add_cancel_l with (multiplicity (list_to_multiset l) a). rewrite Nat.add_comm; rewrite H0; now rewrite Nat.add_comm. Qed.
imports: Coq(List Multiset Arith Setoid) hydras(decidable_set more_list)