proposition: Lemma pformulas_in_valP X P f: inc f (pformulas_in_val X P) <-> [/\ pformula_in P f, pclosed f& pformula_valid_on X f].
proof: Proof. split; first by move /Zo_P => [/pcformulas_inP [pa pb] pc]; split. by move => [pa pb pc];apply/Zo_P => //; split =>//; apply/pcformulas_inP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)