(
eq:{T
}, L,M:T List. L(~eq)M 
(~eq)(L,M))p,q:
. (p
q) p & q (eq:{T}, L,M:T List. L(
eq)M (eq)(L,M))| Rank | Theorem | Name | ||
| 3 | Thm* Discrete{T} (eq:{T}, L,M:T List. L(~eq)M (~eq)(L,M)) | [list_iso_iff_assert_list_iso_2] | ||
| cites | ||||
| 0 | Thm* p,q:. (pq) p & q | [assert_of_band] | ||
| 2 | Thm* Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M)) | [sublist_iff_assert_sublist_2] |