proposition: Lemma formula_Vomega n: natp n -> sub (Vf formulas_rec n) (universe omega0).
proof: Proof. have H: sub variables (universe omega0) by exact:sub_Nat_Vomega. move:n;apply: Nat_induction. rewrite formulas_rec0 => t /atomic_formulaP [qa qb qc qd qe]. have qf: inc (Q t) (universe omega0). rewrite - qb; apply:pair_in_Vomega; fprops. rewrite - qa;apply:pair_in_Vomega => //;case: qe => ->. apply:sub_Nat_Vomega; apply: NS1. apply:sub_Nat_Vomega; apply: NS0. move => n nN Hr; rewrite (formulas_rec_succ nN) => t /next_formulasP; case. + apply: Hr. + move => [pt Pt Qt]; rewrite - pt; apply: pair_in_Vomega; last by apply: Hr. rewrite Pt; apply:sub_Nat_Vomega; apply: NS3. + move => [qa qb qc qd qe]; rewrite - qa - qc; apply: pair_in_Vomega. rewrite qb; apply:sub_Nat_Vomega; apply: NS2. apply:pair_in_Vomega; fprops. + move => [qa qb qc qd qe]; rewrite - qa - qc; apply: pair_in_Vomega. rewrite qb; apply:sub_Nat_Vomega; apply: NS4. apply: pair_in_Vomega; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)