Nuprl - Proof: hprod ty def 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hprod ty def 1 1

1. 'a : S
2. 'b : S
3. x' : hprod('a; 'b)
4. x'' : hprod('a; 'b)
5. rep_prod(x') = rep_prod(x'')

x' = x''

By:	Unab [`hrep_prod`;`hmk_pair`] THEN Simp THEN StrongAuto

Generated subgoal:

1 5. (a:'a. b:'b. (a = 1of(x'))(b = 2of(x')))
5. =
5. (a:'a. b:'b. (a = 1of(x''))(b = 2of(x'')))
5. 'a'bhbool
x' = x''
2 steps

About:

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