proposition: Lemma bigxm C s : prv ([af C] ---> [af s^+ |` C] :\/: [af s^- |` C]).
proof: Proof. apply: (rMP (s := s :\/: ~~:s)); last exact: axI. rule axOE. - rewrite <- axOIl. do 2 Intro. apply: bigAI => t /fsetU1P [->|inC]; first by Asm. Rev. drop. exact: bigAE. - rewrite <- axOIr. do 2 Intro. apply: bigAI => t /fsetU1P [->|inC]; first by Asm. Rev. drop. exact: bigAE. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)