proposition: Lemma monotoneSetFnMap: forall {A B : Type} (f: A-> B), monotoneSetFn (map f).
proof: Proof. intros. unfolds_base. introv Hs Hin. rw in_map_iff in Hin. exrepnd. apply Hs in Hin1. rw in_map_iff; eexists;eauto. Qed.
imports: UsefulTypes bin_rels Omega