(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(yxxx)
5. InjCase[x]( True ; False) = InjCase(yx. 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