∀ x y, equal x y ⇒ ∀ P, P x ⇒ P y

Axiom equal_leibniz : forall A, forall (x:A), forall (y:A), (equal (A) x y) -> forall (P:(A -> Prop)), (P x) -> P y

axiom equal_leibniz : \forall A. \forall (x:A). \forall (y:A). ((equal) (A) x y) -> \forall (P:A -> Prop). (P x) -> P y

axiom equal_leibniz : forall (A : Type) , forall (x:A) , forall (y:A) , ((((connectives.equal) (A)) (x)) (y)) -> forall (P:(A) -> Prop) , ((P) (x)) -> (P) (y)

equal_leibniz [A:TYPE+] : AXIOM (FORALL(x:A):(FORALL(y:A):(connectives_sttfa.equal[A](x)(y) => (FORALL(P:[A -> bool]):(P(x) => P(y))))))

Printing for OpenTheory is not working at the moment.