proposition: Lemma sfc_box p s : [p]s \in F -> s \in F.
proof: Proof. Proof using sfc_F. by case: p => [a|p1 p2|p1 p2|p|t] /sfc_F => /=; case:(s \in F); rewrite ?andbF. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)