P:(T
), L:T List, x:T. (x 
filter(P;L)) 
(x L) & P(x)x:T. (x nil) Falsel:T List, a,x:T. (x [a / l]) x = a 
(x l)| Rank | Theorem | Name |
| 2 | P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) | [member_filter] |
| cites the following: | ||
| 0 | x:T. (x nil) False | [nil_member] |
| 1 | l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |