proposition: Lemma sup_clos_min (s : Pred T) : forall t, s <=p t -> sup_closed t -> sup_closure s <=p t.
proof: Proof. by move=>t H1 H2 p; move/(_ _ H1 H2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)