proposition: Lemma formula_len_pr x (n := formula_len x): formulap x -> [/\ natp n, inc x (Vf formulas_rec n) & forall m, natp m -> inc x (Vf formulas_rec m) -> n <=c m].
proof: Proof. move => xi;rewrite /n /formula_len; set E := Zo _ _. move:(induction_defined_pr next_formulas atomic_formulas). rewrite -/formulas_rec; move => [pa pb pc pd]. have ne: nonempty E by move:(formula_i1 xi) => [m ma mb]; exists m; apply:Zo_i. have oe: ordinal_set E by move => t /Zo_S /OS_nat. move: (ordinal_setI ne oe) => /Zo_P [ha hb]; split => //. move => m mN xf; split => //; fprops. by move => t ti; apply: (setI_hi ti); apply /Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)