L,M:T List, eq:{T=
}. 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* L,M:T List, eq:{T=}. L(eq)M (eq)(L,M) | [sublist_iff_assert_sublist_2_x] | ||
| 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] |