eq:{T=
}, L:T List. L(
eq)LP:
. P 
P = trueeq:{T=}, u:T, v:T List. v(eq)(u.v)| Rank | Theorem | Name | ||
| 3 | Thm* eq:{T=}, L:T List. L(eq)L | [sublist_reflexive] | ||
| cites | ||||
| 0 | Thm* P:. P P = true | [assert_iff_btrue] | ||
| 2 | Thm* eq:{T=}, u:T, v:T List. v(eq)(u.v) | [sublist_tail1] |