Nuprl - Proof: hfst def 1 1

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

1. 'a : S
2. 'b : S
3. x : hprod('a; 'b)
4. x@0 : 'a
5.

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

1of(x) = x@0

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

Generated subgoal:

1 5. y : 'b
6. (a:'a. b:'b. (a = x@0)(b = y))
6. =
6. (a:'a. b:'b. (a = 1of(x))(b = 2of(x)))
6. ('a 'b hbool)
1of(x) = x@0
1 step

About:

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