proposition: Lemma in_nth3 : forall T a def (l:list T), LIn a l -> {n : nat $ (n < length l) # a = nth n l def}.
proof: Proof. introv Hin. apply in_nth in Hin. exrepnd. exists n. dands; sp. rewrite nth_indep with (d':=a); sp. Qed.
imports: UsefulTypes bin_rels Omega