proposition: Theorem nth2_equiv : forall (A:Type) (l:list A) (n:nat) (def:A) (ev: n < length l), (nth n l def) = nth2 l n ev.
proof: Proof. Abort. Theorem len_flat_map: forall {A B} (f:A->list B) (l: list A), length (flat_map f l) = addl (map (fun x => length (f x)) l) . Proof. induction l; auto. simpl. rewrite length_app. f_equal. auto. Qed.
imports: UsefulTypes bin_rels Omega