PrintForm Definitions Lemmas hol combin Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s thm
  'a,'b,'c:S, x:('a  'b  'c), x@0:('a  'b), x@1:'a.
  x(x@1,x@0(x@1)) = x(x@1,x@0(x@1))
By: RewriteOfThm Thm: hs thm (SimpsetC [`hol_to_nuprl`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol combin Sections HOLlib Doc