proposition: Theorem nth2 : forall {A:Type} (l:list A) (n:nat) (ev: n < length l) , A .
proof: Proof. induction l; simpl. intros. provefalse. inversion ev. intros. destruct (eq_nat_dec n 0). subst. exact a. apply IHl with (n:=(n-1)). destruct n. destruct n0. reflexivity. omega. Qed.
imports: UsefulTypes bin_rels Omega