P:(T
Prop), L:T List. 
x
L.P(x) 
(M,N:T List, x:T. P(x) & L = (M @ (x.N)))P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) 
xM.P(x)| Rank | Theorem | Name | ||
| 2 | Thm* P:(TProp), L:T List. xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N))) | [list_exists_is_member_append_lemma] | ||
| cites | ||||
| 1 | Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x) | [list_exists_append_lemma] |