Nuprl - Proof: himp antisym ax

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: himp antisym ax

all

(

t1:hbool. all

(

t1:hbool. (

t2:hbool. implies

(

t1:hbool. (

t2:hbool. (implies(t1,t2)

(

t1:hbool. (

t2:hbool. ,implies(implies(t2,t1),equal(t1,t2)))))

By:	Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoal:

1 1. t1 :
2. t2 :
3. t1  t2
4. t2  t1
  t1 = t2
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html