proposition: Lemma rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s).
proof: Proof. move/rStar_ind' => A B. by rewrite <- B. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)