(
eq:{T
}, L,M:T List. L = M L(
eq)M)P:
. P 
P = true (eq:{T}, u:T, v:T List. v(eq)(u.v))| Rank | Theorem | Name | ||
| 3 | Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M) | [sublist_weakening_wrt_identity] | ||
| cites | ||||
| 0 | Thm* P:. P P = true | [assert_iff_btrue] | ||
| 2 | Thm* Discrete{T} (eq:{T}, u:T, v:T List. v(eq)(u.v)) | [sublist_tail] |