(4steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: arb wf
  T:S. arb(T)  T
By: Unfold `arb` 0 THEN StrongAuto

Generated subgoal:

1 1. T : S
2. x1 : TVoid
3. lem(T) = inr(x1)
  "uu"  T
3 steps

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc