proposition: Lemma first_item_is_item : forall (x : A) (l : List) (n : nat), first_item x l n -> item x l n.
proof: Proof. simple induction 1; intros. apply item_hd. apply item_tl; trivial with coc core arith datatypes. Qed.
imports: Le Gt List