proposition: Lemma AF_universe': foundation_axiom <-> forall x, universe_i x.
proof: Proof. split; first by apply: AF_universe. by move => h x; apply (universe_AF (h x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)