proposition: Theorem permutation_length : forall l m : list A, permutation l m -> length l = length m.
proof: Proof. intros l m H'; elim H'; simpl in |- *; auto. intros l1 l2 l3 H'0 H'1 H'2 H'3. rewrite <- H'3; auto. Qed.
imports: List ListAux