proposition: Lemma stratified_formula_ax2' i: ordinalp i -> (forall x, inc x (length_smaller_formulas i) <-> formulap x /\ formula_len x <o i).
proof: Proof. move => oi; rewrite /length_smaller_formulas. case: (equal_or_not i \0c) => inz; Ytac0. by move => x; split;[ move/in_set0 | rewrite inz; move => [_ /olt0]]. case: (inc_or_not i Nat) => iN; Ytac0;last first. move => x; split; last by move => []. move => fp; split => //; move:(NS_formula_len fp) => /olt_omegaP h. case: (oleT_el OS_omega oi) =>// h'; first by apply: (olt_leT h h'). by case/olt_omegaP: iN. case: (cpred_pr iN inz); set n := cpred i => nN nv. move => x; split => h. have fx:= (formula_hi nN h); split => //; apply: oclt. move:(formula_len_pr fx) => [pa pb pc]; move:(pc _ nN h); rewrite nv=> h'. by apply /(cltSleP nN). move: h => [h1]; move: (h1) => /formula_len_pr [pa pb pc]. move /(oclt3 (CS_nat pa) (CS_nat iN)); rewrite nv. move /(cltSleP nN) => le; exact:(flength_rec h1 le nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)