proposition: Lemma union_exists X: AS8_def -> exists T, forall t, inc t T <-> exists2 i, inc i X & inc t i.
proof: Proof. move => ax. pose R x y:= inc y X /\ inc x y. have hyp: forall y, exists Y, forall x, R x y-> inc x Y. by move => y; exists y; move => x []. move: (ax R hyp X) => [T tp]; exists T => y. split; first by move/tp =>[u ua [ub ucØ]]; ex_tac. by move => [i ia ib]; apply/tp; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)