Nuprl - Proof: hf def 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hf def 1

false

= (

. t)

By:	Simpset [`bequal`] THEN Simp THEN StrongAuto

Generated subgoal:

1 1. t:. t
False
1 step

About:

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