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

By:	((Last (EquandMap (f.f(x@1,y)) )) THEN (Analyze 3)) THEN Simp

None

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