IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hinl def12 1. 'b : S
2. 'a : S
3. e : 'a 4. inl(e) = abs_sum(rep_sum(inl(e)))
inl(e) = abs_sum(b:hbool. x:'a. y:'b. (x =e)b)
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
inl(e) = abs_sum(
b:hbool. 
e)
b)
