proposition: Lemma pfs_V p E a: partition_s p E -> inc a p -> Vf (part_fun p E) a = a.
proof: Proof. by move => pa; apply: ci_V => //; apply/setP_P; apply: partition_set_in_PP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)