proposition: Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.
proof: Proof. intros l l' x Hperm; induction Hperm; simpl; tauto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat