proposition: Lemma rStarE_ind p s t : prv (s ---> t) -> prv (EX p t ---> t) -> prv (EX (p^*) s ---> t).
proof: Proof. move => A B. rewrite <- (axDNE t). rule ax_contraNN. apply: rStar_ind; last by rule ax_contraNN. rule ax_contra. rewrite -> B. exact: axDNI. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)