(6steps total) PrintForm Definitions sqequal 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bool sq 1 1
1. x : Unit+Unit
2. y : Unit+Unit
3. x = y
4. InjCase[x]( x ; x) = InjCase(y; x. x, x)
5. InjCase[x]( True ; False) = InjCase(y; x. True, False)
  x ~ y
By: Assert (True = False)

Generated subgoals:

1   True = False
2 steps
2 6. True = False
  x ~ y
1 step

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

(6steps total) PrintForm Definitions sqequal 1 Sections StandardLIB Doc