proposition: Lemma afa_ex5 X A: X = gfunctions X A <-> (exists a f, [/\ A = singleton a, X = singleton f & f = singleton (J f a)]).
proof: Proof. split; last first. move => [a [f [Aa Xf fv]]]. symmetry; rewrite {2} Xf. apply set1_pr. move: (simple_fct2 f a) => [sa sb _ _ _]. apply /gfunctions_P1; rewrite fv sb; split => //. move => t /set1_P; rewrite Aa Xf => ->; apply: setXp_i; fprops. move => e /gfunctions_P1 [pa pb pc]; rewrite fv. apply: set1_pr1. apply /domain_set0P; rewrite pb Xf; fprops. move => z ze; move: (pc _ ze); rewrite Aa Xf. by move /setX_P => [qa ] /set1_P qb/set1_P qc; rewrite - qa qb qc. move => xsg. case: (emptyset_dichot X) => xne. by empty_tac1 emptyset; rewrite {2} xsg xne gfunctions_empty; apply:set1_1. move: xne => [f fX]. move: (fX); rewrite xsg; move => /gfunctions_P2 [pa pb pc]. set a := Vg f f. have aA: inc a A. apply: pc; apply /range_gP => //; rewrite pb; ex_tac. case: (equal_or_not A (singleton a)) => Aa. have pd: gfunctions X A = singleton f. apply: set1_pr; first by ue. move => z /gfunctions_P2 [qa qb qc]. apply: fgraph_exten => //; first by ue. move => t td /=. have: inc (Vg z t) A by apply qc; apply /(range_gP qa); ex_tac. have: inc (Vg f t) A. by apply pc; apply /(range_gP pa); rewrite pb - qb; ex_tac. by rewrite Aa; move => /set1_P -> /set1_P ->. exists a; exists f;split => //. apply: set1_pr; first by apply: fdomain_pr1 => //; rewrite pb. move => e zf; rewrite (in_graph_V pa zf). by move: (domain_i1 zf); rewrite pb xsg pd => /set1_P ->. 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 F := Lg X (fun z => Yo (Vg z z = a) b a). have fgf: fgraph F by rewrite /F; fprops. have df: domain F = X by rewrite /F; aw. have fx: inc F X. rewrite xsg; apply /gfunctions_P2;split => //. by move => t /(range_gP fgf) [x qa ->]; rewrite /F LgV//; try ue; Ytac h. case: (equal_or_not (Vg F F) a) => eq1. move: (eq1); rewrite {1} /F LgV//; Ytac0 => eba; by case: ba. by move: (eq1); rewrite {1} /F LgV//; Ytac0; case. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)