Nuprl - Proof: his sum rep wd 1 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: his sum rep wd 1 2 2

1. 'a : S
2. 'b : S
3. f : hbool

hbool
4. 'a
5. v2 : 'b
6. f = (

b:hbool.

x@0:'a.

y:'b. (y =

v2)

u:'a+'b. f = rep_sum(u)

By:	DTerm inr(v2) 0 THEN StrongAuto THEN Unab [`hrep_sum`] THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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