proposition: Lemma free_vars_rec x: formulap x -> free_vars x = free_vars_aux x (Lg (small_formulas (formula_len x)) free_vars).
proof: Proof. exact:(stratified_formula_rec free_vars_aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)