proposition: Lemma in_nth : forall T a (l:list T), LIn a l -> {n : nat $ (n < length l) # a = nth n l a}.
proof: Proof. intros ? ? ?. induction l; intros Hin. - simpl in Hin. contradiction. - simpl in Hin. dorn Hin. + intros. subst. exists 0. split; auto. simpl. omega. + intros. apply IHl in Hin. exrepnd. simpl. exists (S n) ;split ; try (simpl; omega). fold (app [a0] l);sp. Qed.
imports: UsefulTypes bin_rels Omega