proposition: Lemma fun_supP (s : Pred tp) (p : tp) : p \In s -> p <== fun_sup s.
proof: Proof. by move=>H x; apply: supP; exists p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)