f:(A
), L:A List. 0<||L|| 
(
a
L.(xL.f(x)
f(a)))a,x:T. (x [a]) 
x = aP:(TProp). (xnil.P(x))P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) 
(yL.P(y))P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))| Rank | Theorem | Name |
| 3 | f:(A), L:A List. 0<||L|| (aL.(xL.f(x)f(a))) | [maximal-in-list] |
| cites the following: | ||
| 0 | a,x:T. (x [a]) x = a | [member_singleton] |
| 0 | P:(TProp). (xnil.P(x)) | [l_all_nil] |
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y)) | [l_exists_cons] |
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) | [l_all_cons] |