proposition: Lemma rStar_eq s p q : (forall t, prv ([p]t <--> [q]t)) -> prv ([p^*]s <--> [q^*]s).
proof: Proof. move => H. rule axEI. - apply: rStar_ind;rewrite -/(Imp_op _ _);[|apply: axStarEl]. rewrite <- H. exact: axStarEr. - apply: rStar_ind;rewrite -/(Imp_op _ _);[|apply: axStarEl]. rewrite -> H. exact: axStarEr. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)