proposition: Lemma formula_sub_rec n m: n <=c m -> natp m -> sub (Vf formulas_rec n) (Vf formulas_rec m).
proof: Proof. move => nm mN. move:(NS_le_nat nm mN) => nN. move:(NS_diff n mN);rewrite -{2} (cdiff_pr nm); move:(m -c n). apply: Nat_induction; first by rewrite (csum0r (proj31 nm)). move => p pN hrec; rewrite (csum_nS _ pN) formulas_rec_succ; fprops. move => t ta; apply/next_formulasP; constructor 1; apply: hrec => //. by apply:NS_sum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)