(4steps total) PrintForm sqequal 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bool cases sqequal 1
1. b : 
  (b ~ true)  (b ~ false)
By: Analyze 1 THEN Analyze 1 THEN Thin 1 THEN Unfolds [`btrue`;`bfalse`] 0
THEN
Fold `it` 0

Generated subgoals:

1   (inl() ~ inl())  (inl() ~ inr())
1 step
2   (inr() ~ inl())  (inr() ~ inr())
1 step

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

(4steps total) PrintForm sqequal 1 Sections StandardLIB Doc