proposition: Lemma not_hint_max C : C \in PU -> maximal F C -> ~~ hintikka C -> prv ([af C] ---> Bot).
proof: Proof. Proof using sfc_F. move/powersetP => Csub /allP => M. rewrite negb_and. case/orP; first exact: ax_lcons. case/allPn => s inC /=. move: (Csub _ inC). move/flip_drop_sign. case: s inC. case => [|x|s t|[a|p0 p1|p0 p1|p|s] t] [|] //= inC inF. - move: (sfc_F inF) => /=. case/andP => sinF tinF. rewrite negb_or. case/andP => /negbTE sninC /negbTE tninC. move: (M s sinF). rewrite sninC orbF => sinC. move: (M t tinF). rewrite tninC /= => tinC. do 2 rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ tinC) at 1. rewrite -> (bigAE _ sinC) => /=. exact: ax_contraNN. - move: (sfc_F inF) => /=. case/andP => sinF tinF. rewrite negb_and. case/orP => [/negbTE sninC | /negbTE tninC]. + move: (M s sinF). rewrite sninC /= => sinC. rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ sinC). do 2 Intro. Apply* 1. Intro. rewrite <- (axBE t). by Apply* 1. + move: (M t tinF). rewrite tninC orbF => tinC. rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ tinC). do 2 Intro. Apply* 1. Intro. by Asm. - move: (sfc_F inF) => /=. case/and3P => inF0 inF1 _. rewrite negb_and. case/orP => [/negbTE ninC0 | /negbTE ninC1]. + move: (M _ inF0). rewrite ninC0 /= => inC0. rule axDup. rewrite -> (bigAE _ inC0) at 1. rewrite -> (bigAE _ inC) => /=. rewrite -> axChEl. exact: axI. + move: (M _ inF1). rewrite ninC1 /= => inC1. rule axDup. rewrite -> (bigAE _ inC1) at 1. rewrite -> (bigAE _ inC) => /=. rewrite -> axChEr. exact: axI. - move: (sfc_F inF). case/and3P => inF0 inF1 _. rewrite negb_or. case/andP => /negbTE ninC0 /negbTE ninC1. move: (M _ inF0) (M _ inF1). rewrite ninC0 ninC1 !orbF => inC0 inC1. do 2 rule axDup. rewrite -> (bigAE _ inC0) at 1. rewrite -> (bigAE _ inC1) at 1. rewrite -> (bigAE _ inC) => /=. rewrite -> (axDNE [p0 + p1]t). exact: axCh. - move/negbTE => ninC. move: (sfc_F inF). case/andP => inF' _. move: (M _ inF'). rewrite ninC /= => inC'. rule axDup. rewrite -> (bigAE _ inC') at 1. rewrite -> (bigAE _ inC) => /=. rewrite -> axConE. exact: axI. - move/negbTE => ninC. move: (sfc_F inF). case/andP => inF' _. move: (M _ inF'). rewrite ninC orbF => inC'. rule axDup. rewrite -> (bigAE _ inC') at 2. rewrite -> (bigAE _ inC) => /=. rewrite <- axCon. exact: axI. - move: (sfc_F inF). case/andP => pinF sinF. rewrite negb_and. case/orP => [/negbTE sninC | /negbTE pninC]. + move: (M _ sinF). rewrite sninC /= => sinC. rule axDup. rewrite -> (bigAE _ sinC) at 1. rewrite -> (bigAE _ inC) => /=. rewrite -> axStarEl. exact: axI. + move: (M _ pinF). rewrite pninC /= => pinC. rule axDup. rewrite -> (bigAE _ inC) at 2 => /=. rewrite -> axStarEr. rewrite -> (bigAE _ pinC) => /=. exact: axI. - move: (sfc_F inF). case/andP => pinF sinF. rewrite negb_or. case/andP => /negbTE sninC /negbTE pninC. move: (M _ pinF) (M _ sinF). rewrite sninC pninC !orbF => pinC sinC. do 2 rule axDup. rewrite -> (bigAE _ inC) at 3 => /=. rewrite -> (axDNE [p^*]t). rewrite -> (bigAE _ sinC) at 1. rewrite -> (bigAE _ pinC). exact: axStar. - move: (sfc_F inF) => /=. case/andP => sinF tinF. rewrite negb_or. case/andP => /negbTE sninC /negbTE tninC. move: (M s sinF). rewrite sninC orbF => sinC. move: (M t tinF). rewrite tninC /= => tinC. do 2 rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ tinC) at 1. rewrite -> (bigAE _ sinC) => /=. rewrite -> axTestE. exact: ax_contraNN. - move: (sfc_F inF) => /=. case/andP => sinF tinF. rewrite negb_and. case/orP => [/negbTE sninC | /negbTE tninC]. + move: (M s sinF). rewrite sninC /= => sinC. rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ sinC). rewrite /=. rewrite <- axTestI. do 2 Intro. Apply* 1. Intro. rewrite <- (axBE t). by Apply* 1. + move: (M t tinF). rewrite tninC orbF => tinC. rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite /=. rewrite <- axTestI. rewrite -> (bigAE _ tinC). do 2 Intro. Apply* 1. Intro. by Asm. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)