proposition: Lemma afa_ex10 X : X = functions X X <-> (exists2 f, X = singleton f & f = triple X X (singleton (J f f))).
proof: Proof. have aux: forall f, X = singleton f -> triple X X (singleton (J f f)) = Lf (fun _ : Set => f) X X. move => f Xf;move: (simple_fct2 f f); set g := (singleton (J f f)). move => [fgg sb sc sd se]. have pa: lf_axiom (fun _ => f) X X by move => s _ ; rewrite Xf;apply: set1_1. apply function_exten; aw; trivial. + by rewrite Xf;apply: function_pr => //; rewrite sc. + by apply: lf_function. + move => t tx /=; rewrite {1} /Vf. rewrite LfV//; aw. by move: tx; rewrite Xf => /set1_P => ->. apply: (iff_trans (afa_ex9 X X)); split. move => [a [f [xa xb xc]]]; exists f => //; move: xc. rewrite xb in xa; rewrite -(set1_inj xa) => {1} ->. by symmetry; apply: aux. by move => [f Xf tf]; exists f, f;split => //; rewrite {1} tf; apply: aux. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)