IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hsnd def12 1. 'a : S
2. 'b : S
3. x : hprod('a; 'b)
y:'b, x@1:'a. mk_pair(x@1,y) = rep_prod(x)
By:
((DTerm 2of(x) 0) THEN (DTerm 1of(x) 0) THEN (Unab [`hrep_prod`;`hmk_pair`]))
THEN
Simp
THEN
StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
y:'b, x@1:'a. mk_pair(x@1,y) = rep_prod(x)
