proposition: Lemma name_unique_first : forall (x : name) (l : prt_names) (n : nat), item _ x l n -> name_unique l -> first_item _ x l n.
proof: Proof. simple induction 1; intros. auto with coc core arith datatypes. apply fit_tl; auto with coc core arith datatypes. apply H1. red in |- *; intros. cut (S m = S n1); intros. injection H5; auto with coc core arith datatypes. elim H2 with (S m) (S n1) x0; auto with coc core arith datatypes. red in |- *; intros. cut (0 = S n0); intros. discriminate H4. elim H2 with 0 (S n0) x; auto with coc core arith datatypes. rewrite H3; auto with coc core arith datatypes. Qed.
imports: Arith MyList MlTypes