proposition: Lemma unionf_exists I (f: fterm): AS8_def -> exists T, forall t, inc t T <-> (exists2 y, inc y I & inc t (f y)).
proof: Proof. move => ax. pose R x y:= inc y I /\ inc x (f y). have hyp: forall y, exists Y, forall x, R x y-> inc x Y. by move => y; exists (f y); move => x []. move: (ax R hyp I) => [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)