proposition: Lemma sup_appE A (B : lattice) (s : Pred (A -> B)) (x : A) : sup s x = sup [Pred y : B | exists f, f \In s /\ y = f x].
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)