EQ:{T=
}, eq:{T
}, L,M:T List. L(
eq)M 
(z:T. z(
EQ) L 
z(eq) M)eq:{T=}, P:(T
Prop), L:T List. xL.P(x) (z:T. z(eq) L P(z))| Rank | Theorem | Name | ||
| 2 | Thm* EQ:{T=}, eq:{T}, L,M:T List. L(eq)M (z:T. z(EQ) L z(eq) M) | [sublist_list_all_lemma] | ||
| cites | ||||
| 1 | Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) | [list_all_is_member_lemma] |