(
eq:{T
}, L,M:T List. L = M L(~eq)M) (eq:{T}, L,M:T List. L = M L(
eq)M)| Rank | Theorem | Name | ||
| 4 | Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(~eq)M) | [list_iso_weakening_wrt_identity] | ||
| cites | ||||
| 3 | Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M) | [sublist_weakening_wrt_identity] |