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

Definition

leibniz.leibniz

Body

λx. λy. ∀ P, P x ⇒ P y

Main Dependencies
Theory

Coq-Jumb
Body

Definition leibniz : forall (A:Type), A -> A -> Prop := fun (A:Type) => fun (x:A) => fun (y:A) => forall (P:(A -> Prop)), (P x) -> P y



Matita-Jumb
Body

definition leibniz : \forall A : Type[0] . A -> A -> Prop := \lambda A : Type[0]. \lambda x : A. \lambda y : A. \forall (P:A -> Prop). (P x) -> P y



Lean-jumb
Body

def leibniz : forall (A : Type) , (A) -> (A) -> Prop := fun (A : Type) , fun (x : A) , fun (y : A) , forall (P:(A) -> Prop) , ((P) (x)) -> (P) (y)



PVS-jumb

Body

leibniz [A:TYPE+] : [A -> [A -> bool]] = (LAMBDA(x:A):(LAMBDA(y:A):(FORALL(P:[A -> bool]):(P(x) => P(y)))))



OpenTheory

Printing for OpenTheory is not working at the moment.