(
eq:{T
}, L,M:T List. L(
eq)M 
(eq)(L,M))p,q:
. (p
q) p & qL:T List, P:(T
). x
L.P(x) xL.P(x)| Rank | Theorem | Name | ||
| 2 | Thm* Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M)) | [sublist_iff_assert_sublist_2] | ||
| cites | ||||
| 0 | Thm* p,q:. (pq) p & q | [assert_of_band] | ||
| 1 | Thm* L:T List, P:(T). xL.P(x) xL.P(x) | [list_all_iff_assert_list_all_2] |