proposition: Lemma pruneE x S : x \in prune S -> ~~ p x (prune S).
proof: Proof. move: S. apply: (nat_size_ind (f := fun X : {fset T} => size X)) => S IH. rewrite prune_equation. case: (fpickP _) => [y pyS yinS|]; last exact. apply: IH. apply: proper_size. exact: properD1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)