Nuprl - Proof: eval factorization one c 1

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

1. a : {2...}
2. b :

3. f : {a..b

}

{a..b

}(f) = 1

(

i:{a..b

}. f(i) = 0)

{a..b

}(f) = 1

f = (

x.0)

By:	SimilarTo: Hyp:-1 ...

Generated subgoals:

1 4. {a..b}(f) = 1
5. i:{a..b}. f(i) = 0
f = (x.0)
1 step

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

About:

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

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