proposition: Lemma formula_val_ic X x f: formulap x -> closed_formula x -> inc f (formula_val X x) -> f = emptyset.
proof: Proof. move => pa pb pc. move: (formula_val_i pa pc);rewrite /formula_values pb. by move /gfunctions_P2 => [_ /domain_set0_P -> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)