proposition: Lemma list_permut_length : forall l1 l2, list_permut l1 l2 -> length l1 = length l2.
proof: Proof. induction l1; intros l2 H. rewrite (list_permut_nil (list_permut_sym H)); auto. elim (In_dec eq_elt_dec a l2). intro Inal2; generalize (split_list_app_cons eq_elt_dec a l2 Inal2); destruct (split_list eq_elt_dec l2 a); intro; subst l2. rewrite list_app_length; simpl; rewrite (IHl1 _ (list_permut_remove_hd l l0 H)); rewrite list_app_length; auto with arith. intro notInal2; absurd (In a l2); trivial; apply in_permut_in with (a :: l1); trivial; left; trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid