P:(T
), L:T List. (x
L.P(x)) 
filter(P;L) = LP:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L)| Rank | Theorem | Name |
| 4 | P:(T), L:T List. (xL.P(x)) filter(P;L) = L | [filter_trivial2] |
| cites the following: | ||
| 3 | P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L) | [filter_trivial] |