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