fact: Definition sup_closure (T : lattice) (s : Pred T) := [Pred p : T | forall t : Pred T, s <=p t -> t \In sup_closed T -> p \In t].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)