proposition: Fact prv_Sprv s : prv s <-> S.prv s.
proof: Proof. split. - elim => {s}; try by constructor. + move => ? ? ? ? ?. exact: S.rMP. + move => u s _ IH1 _ IH2. have H1 : S.prv (AG (u ---> AX u)). exact: S.rNecS. have H2 : S.prv (AG (u ---> s)). exact: S.rNecS. S_rule S.axS. S_rule S.axK. S_rule S.axNS. apply H2. by S_rule S.axSeg. - elim => {s}; try by constructor. + move => ? ? ? ? ?. exact: rMP. + move => t. exact: segerberg. + move => s t. exact: axAGN. + move => s _ . exact: rNecS. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)