proposition: Lemma ax_conv_star p s : prv ([(p^*)^^]s <--> [(p^^)^*]s).
proof: Proof. rule axEI. - suff T q t : prv (t ---> [q^^^*](EX (q^*) t)). { rewrite -> (T p [(p^*)^^]s). apply: rNorm. rewrite -> (ax_convEF). exact: axI. } rule ax_contra. rewrite -> dmAX. rewrite /EX. rewrite -> axDNE. set u := ~~: t. rewrite <- (axStarEl q u) at 2. apply: rStarE_ind; first exact: axI. rewrite -> (axStarEr q u) at 1. rewrite -> ax_convEB. exact: axI. - rewrite -> (ax_convBB (p^*) [p^^^*]s). apply: rNorm. rewrite <- (axStarEl (p^^) s) at 2. apply: rStarE_ind; first exact: axI. rewrite -> axStarEr at 1. rewrite -> ax_convEF. exact: axI. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)