a:{2...}, b:
, f:({a..b
}
). 
{a..b}(f) = 1 
f = (
x.0)a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 (i:{a..b}. f(i) = 0)| Rank | Theorem | Name |
| 6 | a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 f = (x.0) | [eval_factorization_one_c] |
| cites the following: | ||
| 5 | a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 (i:{a..b}. f(i) = 0) | [eval_factorization_one] |