proposition: Lemma Zo_exists E (p: property): AS8_def -> exists F, forall x, inc x F <-> inc x E /\ p x.
proof: Proof. move => ax. pose R (x y: Set) := inc x E /\ p x. have hyp: forall y, exists Y, forall x, R x y-> inc x Y. by move => y; exists E => x []. move: (ax R hyp E) => [T tp]; exists T => y; split. by move/tp => [Y _]. by move => [qa qb]; apply/tp; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)