proposition: Lemma formula_hi x n: natp n -> inc x (Vf formulas_rec n) -> formulap x.
proof: Proof. move:(induction_defined_pr next_formulas atomic_formulas) => [h1 [h2 _] _ _]. move => nV xf; apply/ setU_P; exists(Vf formulas_rec n) => //; Wtac; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)