proposition: Lemma base0P C : C \in U -> prv ([af C] ---> \or_(L <- base [fset D in U | literalC D] C) [af L]).
proof: Proof. Proof with try solve [Lbase1|Lbase3|Lbase4] using sfc_F. apply: (@supp_aux _ ssub) => /= {C} ; last by move => ?; exact: sf_ssub. - move => [[|p|s t|s] [|]] //=; try exact: decomp_lit. + apply: (decomp_ab [fset [fset s^-]; [fset t^+]]) => /=... rewrite -[fImp s t]/(s ---> t). rewrite -> (axIO s t). rule axOE. * rewrite -> af1n. apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite -> (af1p t) at 1. apply: (bigOI xaf). by rewrite !inE eqxx. + apply: (decomp_ab [fset [fset s^+; t^-]]) => /=... rewrite -[fImp s t]/(s ---> t). rewrite -> dmI. rewrite -> (af1p s),(af1n t), <- andU at 1. apply: (bigOI xaf). by rewrite inE. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)