Nuprl - Proof: eval factorization one c

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

a:{2...}, b:

, f:({a..b

}

{a..b

}(f) = 1

f = (

x.0)

By:	SimilarTo Thm* a:{2...}, b:, f:({a..b}). Thm* {a..b}(f) = 1 (i:{a..b}. f(i) = 0) ...w

Generated subgoal:

1 1. a : {2...}
2. b :
3. f : {a..b}
4. {a..b}(f) = 1 (i:{a..b}. f(i) = 0)
{a..b}(f) = 1 f = (x.0)
3 steps

About:

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