proposition: Lemma null_map : forall A B, forall f : A -> B, forall l : list A, null (map f l) <=> null l.
proof: Proof. induction l; simpl; sp; split; sp; try (apply null_nil); apply null_cons in H; sp. Qed.
imports: UsefulTypes bin_rels Omega