proposition: Lemma fun_item : forall (u v : A) (e : List) (n : nat), item u e n -> item v e n -> u = v.
proof: Proof. simple induction 1; intros. inversion_clear H0; auto with coc core arith datatypes. inversion_clear H2; auto with coc core arith datatypes. Qed.
imports: Le Gt List