proposition: Lemma is_first_index_unique : forall {T:Type} (l: list T) (t:T) (n1 n2 :nat), is_first_index l t n1 -> is_first_index l t n2 -> n1 = n2.
proof: Proof. unfold is_first_index, not_in_prefix. introv s1s s3s. repnd. assert (n1<n2 \/ n1=n2 \/ n2<n1) as Htri by omega. (dorn Htri);[|(dorn Htri)]; sp; try (apply s1s in Htri); sp; try (apply s3s in Htri); sp. Qed.
imports: UsefulTypes bin_rels Omega