proposition: Lemma afa_ex6 X: X = gfunctions X X <-> (exists2 x, X = singleton x & x = singleton (J x x)).
proof: Proof. split. move/afa_ex5 => [a [f [pa pb pc]]]; exists a => //. by rewrite pa in pb; rewrite {1 2} (set1_inj pb). by move => [x pa pb]; apply /afa_ex5; exists x; exists x. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)