∀ P return, ∀ x, P x ⇒ return ⇒ ex P ⇒ return

Axiom match_ex_prop : forall A, forall (P:(A -> Prop)), forall (return_:Prop), (forall (x:A), (P x) -> return_) -> (ex (A) P) -> return_

axiom match_ex_prop : \forall A. \forall (P:A -> Prop). \forall (return_:Prop). (\forall (x:A). (P x) -> return_) -> ((ex) (A) P) -> return_

axiom match_ex_prop : forall (A : Type) , forall (P:(A) -> Prop) , forall (return:Prop) , (forall (x:A) , ((P) (x)) -> return) -> (((connectives.ex) (A)) (P)) -> return

match_ex_prop [A:TYPE+] : AXIOM (FORALL(P:[A -> bool]):(FORALL(return:bool):((FORALL(x:A):(P(x) => return)) => (connectives_sttfa.sttfa_ex[A](P) => return))))

Printing for OpenTheory is not working at the moment.