proposition: Theorem firstn_In : forall (A : Type) n (ls : list A)(a : A), In a (firstn n ls) -> In a ls.
proof: Proof. induction n; destruct ls; intuition; simpl in *; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation