1. 'a : S
2. 'b : S
3. x : 'a
4. y : 'b
5. x@0 : hprod('a; 'b)
6. (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0)))
6. = (a:'a. b:'b. (a = x)(b = y))
  <x,y> = x@0  hprod('a; 'b)

By:	Simp THEN Last (EquandMap (f.f(x,y)) ) THEN Simp THEN StrongAuto

1

6. (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0))) 6. = 6. (a:'a. b:'b. (a = x)(b = y)) 6.  ('a  'b  hbool) 7. x = 1of(x@0) 8. y = 2of(x@0)   <x,y> = x@0  hprod('a; 'b)

1 step

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