proposition: Lemma stratified_formula_ax2: (forall i,ordinalp i -> exists E, forall x, inc x E <-> formulap x /\ formula_len x <o i).
proof: Proof. move => i oi;exists (length_smaller_formulas i). by apply:stratified_formula_ax2'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)