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

Axiom

logic.refl

Statement

∀ x, x = x

Main Dependencies
constant
logic.eq
Theory
constant
logic.eq
Coq-Jumb
Statement

Axiom refl : forall A, forall (x:A), eq (A) x x


Matita-Jumb
Statement

axiom refl : \forall A. \forall (x:A). (eq) (A) x x


Lean-jumb
Statement

axiom refl : forall (A : Type) , forall (x:A) , (((logic.eq_) (A)) (x)) (x)


PVS-jumb
Statement

refl [A:TYPE+] : AXIOM (FORALL(x:A):logic_sttfa.eq[A](x)(x))


OpenTheory

Printing for OpenTheory is not working at the moment.