proposition: Lemma fun_supM (s : Pred tp) (p : tp) : (forall q, q \In s -> q <== p) -> fun_sup s <== p.
proof: Proof. by move=>H t; apply: supM=>x [f][H1] ->; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)