proposition: Lemma axStar p s : prv (s ---> [p][p^*]s ---> [p^*]s).
proof: Proof. apply: rAIL. apply: rStar_ind; last exact: axAEl. rule axAcase. drop. apply: rNorm. ApplyH axAI; [exact: axStarEl |exact: axStarEr]. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)