proposition: Lemma ax_lcons C : ~~ lcons C -> prv ([af C] ---> Bot).
proof: Proof. rewrite negb_and -has_predC negbK. case/orP => [inC|/hasP [[[] //= p [|] //]]]. - rewrite -> (bigAE _ inC). exact: axI. - rewrite negbK => pP pN. rewrite -> (axA2 [af C]). rewrite -> (bigAE _ pP) at 2. rewrite -> (bigAE _ pN). simpl. rule axAcase. exact: axI. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)