proposition: Lemma afa_ex7 X: X = gfunctions X X <-> X = singleton (singleton (singleton X)).
proof: Proof. apply (iff_trans (afa_ex6 X)). have pa: forall t, J t t = singleton (singleton t). by move => t; rewrite kpairE /kpair_def /singleton. split. by move => [a ab]; rewrite pa => s; rewrite ab - s. move => h; exists (singleton (singleton X)) => //. by rewrite pa - h. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)