proposition: Lemma list_permut_remove_hd : forall l l1 l2 a, list_permut (a :: l) (l1 ++ a :: l2) -> list_permut l (l1 ++ l2).
proof: Proof. intros l l1 l2 a; unfold list_permut, meq; simpl; intros H a0; generalize (H a0); rewrite multiplicity_app; rewrite multiplicity_app; simpl; intro H1; apply plus_reg_l with (match eq_elt_dec a a0 with left _ => 1 | right _ => 0 end); rewrite H1; repeat rewrite plus_assoc; apply (f_equal (fun n => n + multiplicity (list_to_multiset l2) a0)); apply plus_comm. Qed.
imports: decidable_set List more_list Multiset Arith Setoid