proposition: Lemma prune_sub S : prune S `<=` S.
proof: Proof. apply prune_myind; first by rewrite subxx. move => x S' _ _ _. apply: sub_trans. exact: fsubDl. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)