proposition: Lemma CNFB_e_p8 x n (f := (CNFB_expos_rec x)): ordinalp x -> natp n -> CNFB_expos_rec_nc x n = emptyset -> ( (forall a, inc a (Vf f n) -> b_critical a) /\ (forall k, natp k -> n <=c k -> Vf f k = Vf f n)).
proof: Proof. move=> ox nB me. pose q m := CNFB_expos_rec_nc x m = emptyset. have pa: forall m, q m -> (forall a, inc a (Vf f m) -> b_critical a). by rewrite /q => m h a aw; ex_middle anc; empty_tac1 a; apply: Zo_i. move: (induction_defined_pr (fun z => union (fun_image z CNFB_expos)) (CNFB_expos x)); rewrite -/ (CNFB_expos_rec x) -/f. move=> [sg sjg gz gnz]. have pb: forall m, natp m -> q m -> (Vf f m = Vf f (csucc m) /\ q (csucc m)). move=> m mB qm. suff h: Vf f m = Vf f (csucc m). by split => //; move: qm; rewrite /q /CNFB_expos_rec_nc h //. rewrite (gnz _ mB); move: (pa _ qm) => ax. move: (CNFB_e_p7 ox mB) => [_ osf]. set_extens t. move => ts; apply /setU_P. move: (ax _ ts) (CNFB_e_p6 (osf _ ts)) => cy [ h _]. move: (h cy) => px; exists (singleton t); first by fprops. apply /funI_P; ex_tac. move /setU_P => [y ty] /funI_P [z zw yv]. move: (ax _ zw) (CNFB_e_p6 (osf _ zw)) => cy [ h _]. by move: ty; rewrite yv (h cy) => /set1_P ->. split; first by apply: pa. suff: forall k : Set, natp k -> n <=c k -> (q k /\ Vf f k = Vf f n). by move=> aux k kB nk; move: (aux _ kB nk) => [ _ ]. apply: Nat_induction. move=> aux; move: me; rewrite (cle0 aux); split => //. move => k kB hrec nsk0. case: (equal_or_not n (csucc k)) => nsk; first by rewrite -nsk //. move: (conj nsk0 nsk); move /(cltSleP kB) => h1. move: (hrec h1) => [pc pd]; move: (pb _ kB pc) => [pe pf]; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)