proposition: Lemma Rc_pos {a s C} : s^- \notin Rc a C.
proof: Proof. apply/negP. case/fimsetP => t. rewrite inE andbC. by case (isCBoxP a t) => // t' ->. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CPDL(PDL_def demo)