IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hprod ty def1211 1. 'a : S
2. 'b : S
3. x : 'a'bhbool
4. x@0 : 'a 5. y : 'b 6. x = (a:'a. b:'b. (a =x@0)(b =y))
x':hprod('a; 'b).
x = (a:'a. b:'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:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html