Nuprl - Proof: hprod ty def 1 1 1

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

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

a:'a.

b:'b. (a =

1of(x'))

(b =

2of(x')))
5. =
5. (

a:'a.

b:'b. (a =

1of(x''))

(b =

2of(x'')))

x' = x''

By:	EquandMap (f.f(1of(x'),2of(x'))) -1 THEN Simp THEN StrongAuto

Generated subgoal:

1 6. 1of(x') = 1of(x'')
7. 2of(x') = 2of(x'')
x' = x''
1 step

About:

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