proposition: Lemma formula_i1 x : formulap x -> exists2 n, natp n & inc x (Vf formulas_rec n).
proof: Proof. move:(induction_defined_pr next_formulas atomic_formulas). rewrite -/formulas_rec; move => [pa [pb1 pb2] pc pd]. move /setU_P => [z za /pb2 [n na nb]]; rewrite /natp - pa; exists n => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)