eq:{T=
}, u:T, v:T List. v(
eq)(u.v)eq:{T=}, P:(T
Prop), L:T List. x
L.P(x) 
(z:T. z(eq) L 
P(z))P:
. P P = true| Rank | Theorem | Name | ||
| 2 | Thm* eq:{T=}, u:T, v:T List. v(eq)(u.v) | [sublist_tail1] | ||
| 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] | ||
| 0 | Thm* P:. P P = true | [assert_iff_btrue] |