(2steps total) PrintForm Definitions hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pair unfold
  'a,'b:S, p:('a'b). p = <1of(p),2of(p)>
By: Id THEN StrongAuto

Generated subgoal:

1 1. 'a : S
2. 'b : S
3. p : 'a'b
  p = <1of(p),2of(p)>
1 step

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

(2steps total) PrintForm Definitions hol pair Sections HOLlib Doc