proposition: Lemma permut_length : forall l1 l2, permutation l1 l2 -> length l1 = length l2.
proof: Proof. induction l1; intros l2 H. - rewrite (permut_nil (permut_sym H)); auto. - assert (H0:=permut_cons_InA H). destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))). subst l2. rewrite app_length. simpl; rewrite <- plus_n_Sm; f_equal. rewrite <- app_length. apply IHl1. apply permut_remove_hd with b. apply permut_trans with (a::l1); auto. revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. rewrite (@if_eqA_rewrite_l a b a0); auto. Qed.
imports: Lia Relations Multiset SetoidList