proposition: Lemma flength_rec x m (n := formula_len x): formulap x -> n <=c m -> natp m -> inc x (Vf formulas_rec m).
proof: Proof. move => fp; move:(formula_len_pr fp) => []; rewrite -/n => nN xv _ nm mN. apply:(formula_sub_rec nm mN xv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)