proposition: Lemma axEOOE p s t : prv (EX p (s :\/: t) ---> EX p s :\/: EX p t).
proof: Proof. rewrite /EX. rewrite <- dmA. rewrite <- (ax_contraNN _ ([p]~~: (s:\/:t))). rewrite -> axABBA. apply: rNorm. rewrite <- dmO. exact: axI. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)