fact: Definition free_vars_aux x f := Yo (P x = val_in \/ P x = val_eq) (doubleton (P (Q x)) (Q (Q x))) (Yo (P x = val_not ) (Vg f (Q x)) (Yo (P x = val_or) (Vg f (P (Q x)) \cup (Vg f (Q (Q x)))) ((Vg f (Q (Q x)) -s1 (P (Q x)))))).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)