proposition: Lemma first_item_unique : forall (x : A) (l : List) (n : nat), first_item x l n -> forall m : nat, first_item x l m -> m = n.
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. elim H2; auto with coc core arith datatypes. generalize H2. inversion_clear H3; intros. elim H3; auto with coc core arith datatypes. elim H1 with n1; auto with coc core arith datatypes. Qed.
imports: Le Gt List