proposition: Lemma prune_D2 : D2 (prune pcond S0).
proof: Proof. move => C /pruneE. rewrite negb_or => /andP [_ P s inC]. rewrite negbK in P. move/allP : P => /(_ _ inC) /fulfillAGP. tauto. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)