proposition: Lemma list_permut_size : forall size l1 l2, list_permut l1 l2 -> list_size size l1 = list_size size l2.
proof: Proof. intro size; induction l1. intros l2 P; rewrite (list_permut_nil (list_permut_sym P)); trivial. intros l2 P; generalize (split_list_app_cons eq_elt_dec _ _ (cons_permut_in P)); destruct (split_list eq_elt_dec l2 a); intro; subst l2; rewrite list_size_app; simpl; rewrite (IHl1 _ (list_permut_remove_hd _ _ P)); rewrite list_size_app; rewrite plus_comm; rewrite <- plus_assoc; apply (f_equal (fun n => list_size size l + n)); apply plus_comm. Qed.
imports: decidable_set List more_list Multiset Arith Setoid