proposition: Lemma afa_ex9 X A: X = functions X A <-> (exists a f, [/\ A = singleton a, X = singleton f & f = Lf (fun _ => a) X A]).
proof: Proof. have res: forall A a f t, function f -> A = singleton a -> target f = A -> inc t (source f) -> Vf f t = a. by move => B a f t ff -> tf tsf;move:(Vf_target ff tsf);rewrite tf => /set1_P. split; last first. move => [a [f [Aa Xf fv]]]. symmetry; rewrite {2} Xf. have la: lf_axiom (fun _ : Set => a) X A by move => t _; rewrite Aa; fprops. have aux: function (Lf (fun _ : Set => a) X A) by apply: lf_function. apply: set1_pr. apply /functionsP; rewrite fv;red;saw. move => e /functionsP [pa pb pc]; rewrite fv. apply function_exten => //; aw; trivial => z ze; rewrite LfV//; last by ue. by apply: (@res A). move => xsg. case: (emptyset_dichot X) => xne. have aux:= (empty_function_tg_function A). by empty_tac1 ( empty_function_tg A); rewrite xsg xne; apply /functionsP. move: xne => [f fX]. move: (fX); rewrite xsg; move => /functionsP [pa pb pc]. set a := Vf f f. have aA: inc a A by rewrite -pc /a; Wtac. case: (equal_or_not A (singleton a)) => Aa. have ha: functions X A = singleton f. apply: set1_pr;first by ue. move => z /functionsP [qa qb qc]. apply: function_exten => //; (try ue); move => t td /=. have tx: inc t (source f) by rewrite pb - qb. by rewrite (res A a f t pa Aa pc tx) (res A a z t qa Aa qc td). have pf: lf_axiom (fun _ => a) (functions X A) A by move => t _. have sf: source f = (functions X A) by ue. exists a, f;split => //. apply: function_exten; aw; trivial. - by apply: lf_function. - move => t tf /=; rewrite LfV//; [ by apply: (@res A) | ue ]. have [b bA ba]: exists2 b, inc b A & b <> a. ex_middle bad; case: Aa; apply: set1_pr => // z zA. ex_middle h; case: bad; ex_tac. set lam := (fun z => Yo (Vf z z = a) b a). have ta: lf_axiom lam X A by rewrite /lam; move => t tX /=; Ytac h. have fx: inc (Lf lam X A) X. rewrite {2} xsg; apply /functionsP;red;saw. by apply: lf_function. by case: (equal_or_not (Vf (Lf lam X A)(Lf lam X A)) a) => eq1; move: (eq1); rewrite LfV//; rewrite {1} /lam; Ytac0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)