// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Axiom

connectives.ex_intro

Statement

∀ P x, P x ⇒ ex P

Main Dependencies
constant
connectives.ex
Theory
constant
connectives.ex
Coq-Jumb
Statement

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


Matita-Jumb
Statement

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


Lean-jumb
Statement

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


PVS-jumb
Statement

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


OpenTheory

Printing for OpenTheory is not working at the moment.