list
3
jlc
Sections
Support(jlc)
Doc
Def
(~
eq)(L,M) == ((
eq)(L,M))
((
eq)(M,L))
is mentioned by
Thm*
Discrete{T}
(
eq:{T
}, L,M:T List. L(~eq)M
(~
eq)(L,M))
[list_iso_iff_assert_list_iso_2]
list
3
jlc
Sections
Support(jlc)
Doc
(
eq:{T
}, L,M:T List. L(~eq)M 
(~eq)(L,M))eq)(L,M) == ((
eq)(L,M))
((eq)(M,L))
(eq:{T}, L,M:T List. L(~eq)M (~eq)(L,M))