proposition: Lemma prune_myind (P : {fset T} -> Type) S : P S -> (forall x S0, p x S0 -> x \in S0 -> P S0 -> S0 `<=` S -> P (S0 `\` [fset x])) -> P (prune S).
proof: Proof. move: S. apply: (nat_size_ind (f := fun X : {fset T} => size X)) => S IH Hp Hstep. rewrite prune_equation. case: (fpickP _) => // x px inS. apply: IH. - apply: proper_size. exact: properD1. - apply: Hstep => //. exact: subxx. - move => y S' py inS' PS' sub. apply: Hstep => //. apply: sub_trans sub _. exact: fsubDl. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)