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

Theorem

leibniz.refl_leibniz

Statement

∀ x, leibniz x x

Main Dependencies
definition
leibniz.leibniz
Theory
Coq-Jumb
Statement

Theorem refl_leibniz : forall A, forall (x:A), leibniz (A) x x.


Matita-Jumb
Statement

theorem refl_leibniz : \forall A. \forall (x:A). (leibniz) (A) x x.


Lean-jumb
Statement

theorem refl_leibniz : forall (A : Type) , forall (x:A) , (((leibniz.leibniz) (A)) (x)) (x).


PVS-jumb
Statement

refl_leibniz [A:TYPE+] : LEMMA (FORALL(x:A):leibniz_sttfa.leibniz[A](x)(x))


OpenTheory

Printing for OpenTheory is not working at the moment.