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