∀ x, equal x x

Axiom refl_equal : forall A, forall (x:A), equal (A) x x

axiom refl_equal : \forall A. \forall (x:A). (equal) (A) x x

axiom refl_equal : forall (A : Type) , forall (x:A) , (((connectives.equal) (A)) (x)) (x)

refl_equal [A:TYPE+] : AXIOM (FORALL(x:A):connectives_sttfa.equal[A](x)(x))

Printing for OpenTheory is not working at the moment.