(10steps total) PrintForm Definitions hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hprod ty def 1 2 1 1

1. 'a : S
2. 'b : S
3. x : 'a'bhbool
4. x@0 : 'a
5. y : 'b
6. x = (a:'ab:'b. (a = x@0)(b = y))
  x':hprod('a'b). 
  x = (a:'ab:'b. (a = 1of(x'))(b = 2of(x')))  'a'bhbool


By: ((DTerm <x@0,y> 0) THEN (H 6 0)) THEN Simp THEN StrongAuto


Generated subgoals:

None

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

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