proposition: Lemma T2toB_surjective x: x <o Gamma_0 -> exists2 y, T2nf y & x = T2toB y.
proof: Proof. move => xo; move:(proj31_1 xo) => ox; move: xo. case:(least_ordinal6 (fun z => z <o Gamma_0 -> exists2 y, T2nf y &z = T2toB y) ox) =>//. set z := least_ordinal _ _. move => [oz Hz []] zo. case: (ozero_dichot oz); first by move => ->; exists zero. move => zp. move: (the_CNF_simplP zp) (CNF_simple_bdn3 zp zo). set aa := (P (the_CNF_simpl z)); set n := (P (Q (the_CNF_simpl z))); set c := (Q (Q (the_CNF_simpl z))); set w := inv_psi_omega _. move => h1 [ra rb rc rd]. move:(CNF_simple_p2 h1) =>[_ cz _]. move: h1 => [qa qb qc qd qe]. move: (nat_to_B_surjective qc) => [n' n'v]. have h: forall t, t <o z -> exists2 y : T2, T2nf y & t = T2toB y. move => t ta; apply: Hz; [by apply/(oltP oz) | exact: (olt_ltT ta zo) ]. move: (h _ rb) => [A an ap]. move: (h _ rc) => [B bn bp]. move: (h _ cz) => [C cn cp]. exists (cons A B n' C); last by rewrite /= - ap -bp - cp - n'v rd qd. have ha: T2nf [A, B] by rewrite nf_psi an bn. have hb:= (OS_pow OS_omega qa). rewrite /= an bn cn /=; apply /(T2toB_mon2 cn ha). move: qe; rewrite {2} /T2toB -/T2toB - ap - bp - cp rd /nat_to_B succ_zero. by rewrite oprod1r // osum0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)