proposition: Lemma first_index {A: Type} (l: list A) (a:A) (deq : Deq A): {n:nat $ n < length l # nth n l a= a #(forall m, m<n -> nth m l a <>a)} [+] (! (LIn a l)).
proof: Proof. induction l as [| h l Hind]; [right;sp;fail|]. destruct (deq h a); subst; allsimpl;[left ; exists 0; sp; omega | ]. dorn Hind. + exrepnd. left. exists (S n0). split; auto; try omega; split; auto. introv Hlt. destruct m; auto. apply Hind0; omega. + right. intro Hc; sp. Defined.
imports: UsefulTypes bin_rels Omega