proposition: Lemma nth_select3: forall (A : Type) (n : nat) (l : list A) (a def : A), n < length l -> (nth n l def) =a -> select n l = Some a.
proof: Proof. introv K1 K2. pose proof (nth_select1 n l def K1). congruence. Qed.
imports: UsefulTypes bin_rels Omega