Nuprl - Proof: eval factorization one 1 1

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

a:{2...}, b:

, f:({a..b

}

(

i:{a..b

}. i

f(i) = 1)

(

i:{a..b

}. f(i) = 0)

By:	Rewrite by Thm* e:({a..b}). ( i:{a..b}. e(i)) = 1 (i:{a..b}. e(i) = 1) ...w

Generated subgoal:

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

About:

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