proposition: Lemma free_vars_not a (x := J val_not a): formulap a -> free_vars x = free_vars a.
proof: Proof. move => pa;move: (fkind_not_p2 pa) => [sa sb]. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. have ha:~(val_not = val_in \/ val_not = val_eq) by case => h; fprops. rewrite (free_vars_rec sa) /free_vars_aux; aw; Ytac0; Ytac0; Ytac0. rewrite LgV//; apply/Zo_P; split => //; rewrite sb. apply: (cltS (NS_formula_len pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)