Nuprl - Proof: hinr def 1 2

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

1. 'a : S
2. 'b : S
3. e : 'b
4. inr(e) = abs_sum(rep_sum(inr(e)))

inr(e) = abs_sum(

b:hbool.

x@0:'a.

y:'b. (y =

By:	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