L:T List, P:(T
). (x
L.P(x)) 
reduce(
x,y. P(x)
y;true;L)P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))| Rank | Theorem | Name |
| 3 | L:T List, P:(T). (xL.P(x)) reduce(x,y. P(x)y;true;L) | [l_all_reduce] |
| cites the following: | ||
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) | [l_all_cons] |