proposition: Lemma sup_clos_idemp (s : Pred T) : sup_closed s -> sup_closure s =p s.
proof: Proof. by move=>p; split; [apply: sup_clos_min | apply: sup_clos_sub]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)