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