proposition: Lemma Permutation_Forall : forall A (P : A → Prop) (xs ys : list A), Permutation xs ys → List.Forall P xs → List.Forall P ys.
proof: Proof. intros. rewrite <- H. assumption. Qed.
imports: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe