Nuprl - Proof: hprod ty def 1 3

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

1. 'a : S
2. 'b : S
3. x : 'a

hbool
4.

x':hprod('a; 'b). x = rep_prod(x')

is_pair(x)

By:	Last Analyze THEN Unab [`hrep_prod`;`his_pair`] THEN Simp THEN StrongAuto

Generated subgoal:

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

About:

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