proposition: Lemma free_vars_variables x: formulap x -> sub (free_vars x) variables /\ finite_set (free_vars x).
proof: Proof. move => fx. move: (formula_len_pr fx) => []; clear fx. move: {1 2} (formula_len x) => n na nb _; move:n na x nb . apply: Nat_induction. rewrite formulas_rec0 => x /atomic_formulaP [sa qa qb qc qd]. suff: (free_vars x) = doubleton (P (Q x)) (Q (Q x)). move => ->; split; first by move => t /set2_P; case => ->. apply: set2_finite. rewrite - {1} sa -{1} qa; case qd => ->. by apply:free_vars_in. by apply:free_vars_eq. move => n nN Hrec x;rewrite (formulas_rec_succ nN); case /next_formulasP. + apply: Hrec. + move => [pa pb pc];move:(formula_hi nN pc) => pd. by move:(free_vars_not pd); rewrite - pb pa => ->; apply: Hrec. + move => [pa pb pc pd pe]. move: (free_vars_or (formula_hi nN pd) (formula_hi nN pe)). move: (Hrec _ pd) => [ua /card_finite_setP ub]. move:(Hrec _ pe) =>[uc /card_finite_setP ud]. rewrite - pb pc pa => ->; split; first ( move => t /setU2_P; case; fprops). move:(NS_sum ub ud) => ue; apply/card_finite_setP. by apply: (NS_le_nat _ ue); rewrite csum2cl csum2cr; apply: csum2_pr6. + move => [pa pb pd pc pe]; move:(formula_hi nN pe) => pf. move:(free_vars_ex pc pf);rewrite pd - pb pa => sa. have sb: sub (free_vars x) (free_vars (Q (Q x))). by rewrite sa; move => t /setC_P []. move:(Hrec _ pe) => [sc sd]; split; first by apply: (sub_trans sb sc). apply: (sub_finite_set sb sd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)