(
eq:{T
}, L,M:T List. (L @ M)(~eq)(M @ L)) (eq:{T}, L,M:T List. (L @ M)(
eq)(M @ L))| Rank | Theorem | Name | ||
| 3 | Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(~eq)(M @ L)) | [append_commutes_under_list_iso] | ||
| cites | ||||
| 2 | Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(eq)(M @ L)) | [append_commutes_under_sublist] |