PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert of bequal
  T:Type, x,y:T. (x = y)  x = y
By: Unfold `bequal` 0 THEN Simp THEN StrongAuto THEN HypBackchain THEN StrongAuto

Generated subgoals:

None

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

PrintForm Definitions hol Sections HOLlib Doc