proposition: Lemma ax_conv p s : prv ([(p^^)^^]s <--> [p]s).
proof: Proof. rule axEI. - rewrite <- (ax_convEF p^^ s) at 2. by rewrite <- (axConvF p [(p^^)^^]s). - rule ax_contra. rewrite -> dmAX. rewrite -> dmAX. rewrite -> (axConvB p (~~: s)) at 1. restore. by rewrite -> ax_convEB. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)