proposition: Lemma segerberg p s : prv ([p^*](s ---> [p]s) ---> s ---> [p^*]s).
proof: Proof. pose u := [p^*](s ---> [p]s) :/\: s. suff S : prv (u ---> [p]u). { apply: rAIL. rewrite -/u. apply: rStar_ind S _. exact: axAEr. } rewrite /u. rule axAcase. do 2 Intro. ApplyH axABBA. ApplyH axAI. - Rev* 1. drop. by rewrite -> (axStarEr p (s ---> [p]s)) at 1. - Rev. Rev. by rewrite -> (axStarEl p (s ---> [p]s)) at 1. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)