P:(T
Prop), x:T, L:T List. (
y
[x / L].P(y)) 
P(x) 
(yL.P(y))l:T List, a,x:T. (x [a / l]) x = a (x l)| Rank | Theorem | Name |
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y)) | [l_exists_cons] |
| cites the following: | ||
| 1 | l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |