proposition: Lemma forall_permutation: forall A P (L : list A), Forall P L -> forall L', Permutation L L' -> Forall P L'.
proof: Proof. intros. revert H. induction H0; intros; auto. inversion H; subst. constructor; auto. inversion H. inversion H3. subst. repeat (constructor; auto). Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset