proposition: Lemma baseP C : C \in U -> prv ([af C] ---> \or_(D <- base S C) [af D]).
proof: Proof. Proof using coref_S sfc_F. move => inU. rewrite -> base0P => //. apply: bigOE => L. rewrite !inE andbC => /and3P [L1 L2 L3]. case: (boolP (L \in S)) => LS; first by apply: (bigOI xaf); rewrite inE LS. case: (boolP (lcons L)) => LL; last by rewrite -> (ax_lcons LL); exact: axBE. have H : L \in S0 `\` S by rewrite !inE LS LL L2 L3. Intro. ApplyH axBE. Rev. exact: (coref_S H). Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)