proposition: Lemma formulas_rec_succ n: inc n Nat -> Vf formulas_rec (csucc n) = next_formulas (Vf formulas_rec n).
proof: Proof. move:(induction_defined_pr next_formulas atomic_formulas) => [_ _ _ h]. apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)