proposition: Lemma CNFB_exists x: ordinalp x -> exists2 X, CNFB_ax X & CNFBv X = x.
proof: Proof. move => ox. move: (CNFb_exists ox bg2) => [e [c [n [ax nN ->]]]]. move: (CNFbB_prop ax nN); set X := Lg _ _; move => [sa sb]. by exists X. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)