Nuprl - Proof: hfst def 1

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

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

1of(x) = (@

x@0:'a. (

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

(rep_prod(x)))))

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

Generated subgoals:

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

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

About:

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

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