proposition: Lemma neq_contra C D : C \in S -> D \in S -> C != D -> prv ([af C] ---> [af D] ---> fF).
proof: Proof. Proof using sub_S. move => CinS DinS. rewrite eqEsub negb_and. case/orP => H; [exact: nsub_contra | rule axC; exact: nsub_contra]. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)