(6steps total) PrintForm sqequal 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bool sq 1
1. x : 
2. y : 
3. x = y
  x ~ y
By: let T  Unfold `bool` in
(T 1 THEN T 2 THEN T 3 THEN ApFunToHypEquands `z' InjCase(z; x. x, x) Unit 3)
THEN
(ApFunToHypEquands `z' InjCase(z; x. True, False) Prop 3)

Generated subgoal:

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
4 steps

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

(6steps total) PrintForm sqequal 1 Sections StandardLIB Doc