proposition: Theorem nth3 : forall {A:Type} (l:list A) (n:nat) (ev: n < length l) , {x:A | nth n l x =x} .
proof: Proof. induction l; simpl. intros. provefalse. inversion ev. intros. destruct n . subst. exact (exist (eq a) a eq_refl ). apply IHl with (n:=(n)). omega. Qed.
imports: UsefulTypes bin_rels Omega