proposition: Lemma free_vars_in b c (x := J val_in (J b c)): variablep b -> variablep c -> free_vars x = doubleton b c.
proof: Proof. move => pb pc. have ha: (val_in = val_in \/ val_in = val_eq) by left. have fx: formulap x by exact (proj1 (fkind_in_p2 pb pc)). by rewrite (free_vars_rec fx) /free_vars_aux /x; aw; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)