eq:{T=
}, u:T, L:T List. u(
eq) L 
(
v:T, M:T List. L = v.M)eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)))| Theorem | Name | ||
| Thm* eq:{T=}, u:T, L:T List. u(eq) L (v:T, M:T List. L = v.M) | [is_member_non_nil] | ||
| cites | |||
| Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N))) | [is_member_append_lemma] |