proposition: Theorem hd_error_Some_In : forall (A : Type)(ls : list A) a, hd_error ls = Some a -> In a ls.
proof: Proof. intuition. destruct ls; simpl in *. discriminate. inversion H; clear H; subst. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation