proposition: Lemma extension0 C : C \in PU -> prv ([af C] ---> \or_(D <- [fset D in S0 | C `<=` D]) [af D]).
proof: Proof. Proof using sfc_F. rewrite powersetE. apply: (slack_ind (P := fun C => prv ([af C] ---> _))) => D IH sub. case (boolP (maximal F D)). - case (boolP (hintikka D)). + move => H M. apply: bigOI. by rewrite !inE powersetE sub H M /= subxx. + move: sub. rewrite -powersetE => sub nH M. rewrite -> (not_hint_max sub M nH). exact: axBE. - case/allPn => s inF /=. rewrite negb_or. case/andP => sninD fsninD. rewrite -> (bigxm D s). rule axOE; (rewrite -> IH; last by rewrite fproper1). + apply: or_sub. move => E. rewrite !inE. case/andP => /and3P [-> -> ->] /=. by case/fsubUsetP. + rewrite fsubUset sub fsub1 /= andbT. apply/cupP. exists s. by rewrite inF !inE eqxx. + apply: or_sub. move => E. rewrite !inE. case/andP => /and3P [-> -> ->] /=. by case/fsubUsetP. + rewrite fsubUset sub fsub1 /= andbT. apply/cupP. exists s. by rewrite inF !inE eqxx. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)