P:(T
Prop), L,M:T List. 
x
(L @ M).P(x) 
xL.P(x) 
xM.P(x)L:T List. (L @ nil) = L| Theorem | Name | ||
| Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x) | [list_exists_append_lemma] | ||
| cites | |||
| Thm* L:T List. (L @ nil) = L | [append_nil_right_identity] |