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