Nuprl - Proof: hcomma def 1 1 1

(7steps total) PrintForm Definitions hol pair Sections HOLlib Doc

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

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

<x,y> = (@x@0:hprod('a; 'b). ((rep_prod(x@0)) =

(mk_pair(x,y))))

By:	Unab [`hrep_prod`;`hmk_pair`] THEN ChooseDC THEN Try (Unfold `label` 0)

Generated subgoals:

1 5. x@0 : hprod('a; 'b)
6. (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0)))
6. = (a:'a. b:'b. (a = x)(b = y))
  <x,y> = x@0  hprod('a; 'b)
2 steps

2   x@0:hprod('a; 'b).
  (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0)))
  = (a:'a. b:'b. (a = x)(b = y))
1 step

About:

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

(7steps total) PrintForm Definitions hol pair Sections HOLlib Doc

1	5. x@0 : hprod('a; 'b) 6. (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0))) 6. = (a:'a. b:'b. (a = x)(b = y)) <x,y> = x@0 hprod('a; 'b)	2 steps
2	x@0:hprod('a; 'b). (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0))) = (a:'a. b:'b. (a = x)(b = y))	1 step