(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 1
1. T : S
2. x1 : TVoid
3. lem(T) = inr(x1)
  "uu"  T
By: Analyze 1 THEN StrongAuto

Generated subgoal:

1 1. T : Type
2. x:T. True
3. x1 : TVoid
4. lem(T) = inr(x1)
  "uu"  T
2 steps

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc