proposition: Lemma ax_lcons C : ~~ lcons C -> prv ([af C] ---> Bot).
proof: Proof. rewrite negb_and -has_predC negbK. case/orP => [inC|/hasP [s sinC /=]]. - rewrite -> (bigAE _ inC). exact: axI. - rewrite negbK => nsinC. rewrite -> (axA2 [af C]). rewrite -> (bigAE _ sinC) at 2. rewrite -> (bigAE _ nsinC). simpl. rule axAcase. case: s sinC nsinC => s [|] _ _ /=. exact: axI. exact: axContra. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)