(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
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)
  True = False
By: Analyze 0

Generated subgoal:

1 6. True = False
  False
1 step

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

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