proposition: Lemma stratified_formula_rec (H : fterm2) (f := stratified_fct formulap H formula_len): (forall x, formulap x -> f x = H x (Lg (small_formulas (formula_len x)) f)).
proof: Proof. move => x fx; rewrite {1} /f. rewrite(stratified_fct_pr H stratified_formula_ax1 stratified_formula_ax2 fx). congr (H x (Lg _ f)). have nN:= (NS_formula_len fx). move: (stratified_setP stratified_formula_ax2 (OS_nat nN)) => h. set_extens y. move /h =>[pa pb]; apply:Zo_i => //. have pc := (NS_formula_len pa). exact :(oclt3 (CS_nat pc) (CS_nat nN)). by move => /Zo_P [ffx / oclt lt]; apply/h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)