proposition: Theorem fst_split_as_map: forall {A B :Type} (sub : list (A * B)), fst (split sub) = map (fun p=> fst p) sub.
proof: Proof. intros. induction sub as [| vt sub Hind]; auto. simpl. destruct vt as [v t]. simpl. destruct (split sub). allsimpl. f_equal. auto. Qed.
imports: UsefulTypes bin_rels Omega