proposition: Lemma afa_ex11 X : X = functions X X <-> X = singleton (singleton (singleton (singleton (singleton X)))).
proof: Proof. split. move /afa_ex10 => [f ->]. by rewrite /triple ! kpairE /kpair_def - !/(singleton _) => <-. move => h; apply /afa_ex10. exists (singleton (singleton (singleton (singleton X)))); first exact. by rewrite /triple !kpairE /kpair_def -! /(singleton _) -h -! /(singleton _). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)