proposition: Lemma fun_image_exists E (f: fterm): AS8_def -> exists F, forall x, inc x F <-> exists2 y, inc y E & x = f y.
proof: Proof. move => ax. pose R x y:= x = f y /\ inc y E. have hyp: forall y, exists Y, forall x, R x y-> inc x Y. move => y. exists (singleton (f y)); move => x [-> _]; fprops. move: (ax R hyp E) => [T tp]; exists T => y; split. 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)