Nuprl - Proof: hsnd def 1

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

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

2of(x) = (@

y:'b. (

x@0:'a. ((mk_pair(x@0,y)) =

(rep_prod(x)))))

By:	Unab [`bchoose`] THEN ChooseDC THEN Simp THEN StrongAuto

Generated subgoals:

1 4. y : 'b
5. x@1:'a. mk_pair(x@1,y) = rep_prod(x)
2of(x) = y
2 steps

2 y:'b, x@1:'a. mk_pair(x@1,y) = rep_prod(x)
1 step

About:

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

1	4. y : 'b 5. x@1:'a. mk_pair(x@1,y) = rep_prod(x) 2of(x) = y	2 steps
2	y:'b, x@1:'a. mk_pair(x@1,y) = rep_prod(x)	1 step