Nuprl - Proof: fun eq lemma

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun eq lemma

'a:S, f:('a

), x1,x2:'a. f(x1) &

f(x2)

x1 = x2

By:	RewriteOfThm Thm* 'a:S. Thm* all Thm* (f:'a hbool. all Thm* (f:'a hbool. (x1:'a. all Thm* (f:'a hbool. (x1:'a. (x2:'a. implies Thm* (f:'a hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2))) Thm* (f:'a hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2)))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html