proposition: Lemma universe_inaccessible_mo1: replacementA (fun z => inc z (universe a)) inc.
proof: Proof. move => x p f /universe_inaccessible_inc [pa pb] h. exists (fun_image (Zo x p) f); split; last first. move => z za; split. by move /funI_P => [t /Zo_P [ra rb] ->]; exists t => //; apply: pa. by move => [t ta [tx pt ->]]; apply /funI_P; exists t => //; apply /Zo_P. have sc: sub (Zo x p) x by apply: Zo_S. apply /universe_inaccessible_inc; split. by move => t/funI_P [z /Zo_P[ra rb] ->]; apply: h => //; apply: pa. move: (cleT (fun_image_smaller (Zo x p) f) (sub_smaller sc)) => sa. exact: (cle_ltT sa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)