L,M:T List, eq:{T=
}. L(
eq)M 
(eq)(L,M)
(eq:{T
}, L,M:T List. L(eq)M (eq)(L,M))T:Type, L,M:T List, eq:(T
T
). (eq)(L,M) 
T:Type, L,M:T List, eq:(TT). (eq)(L,M) eq)(L,M) == ((eq)(L,M))
((eq)(M,L))eq)(L,M) == xL.x(eq) M
is mentioned by
| Thm* L,M:T List, eq:{T=}. L(eq)M (eq)(L,M) | [sublist_iff_assert_sublist_2_x] |
| Thm* Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M)) | [sublist_iff_assert_sublist_2] |
| Thm* T:Type, L,M:T List, eq:(TT). (eq)(L,M) | [apply_wf_sublist_2] |
| Thm* T:Type, L,M:T List, eq:(TT). (eq)(L,M) | [apply_sublist_2_wf] |
| Def (~eq)(L,M) == ((eq)(L,M))((eq)(M,L)) | [list_iso_2] |