proposition: Lemma list_permut_add_cons_inside : forall a l l1 l2, list_permut l (l1 ++ l2) -> list_permut (a :: l) (l1 ++ a :: l2).
proof: Proof. intros; replace (a :: l) with (nil ++ a :: l); trivial; apply list_permut_add_inside; trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid