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