Nuprl - Proof: eval factorization one

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eval factorization one

a:{2...}, b:

, f:({a..b

}

{a..b

}(f) = 1

(

i:{a..b

}. f(i) = 0)

By:	Def of {<int>..<int>}(<exponents>)

Generated subgoal:

1 a:{2...}, b:, f:({a..b}).
( i:{a..b}. if(i)) = 1 (i:{a..b}. f(i) = 0)
8 steps

About:

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