Thm*  eq:{T  }, L,M:T List. Dec(L(~eq)M) | [decidable__list_iso] |
Thm* Discrete{T}   (eq:{T}, L,M:T List. L(~eq)M  (~eq)(L,M)) | [list_iso_iff_assert_list_iso_2] |
| Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1(~eq3)L3 L2(~eq3)L4) | [list_iso_functionality_wrt_id_list_iso_list_iso] |
| Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(~eq2)L3 L2(~eq2)L4) | [list_iso_functionality_wrt_id_list_iso_id] |
Thm* L1,L2:T List, eq1,eq2,eq3,eq4:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 eq3 = eq4 L1(~eq1)L2 L3(~eq2)L4 (L1( eq3)L3 L2(eq4)L4) | [sublist_functionality_wrt_id_list_iso_list_iso] |
| Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1 = L2 L3(~eq1)L4 (L1(eq2)L3 L2(eq2)L4) | [sublist_functionality_wrt_id_id_list_iso] |
| Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(eq2)L3 L2(eq2)L4) | [sublist_functionality_wrt_id_list_iso_id] |
| Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1 @ L3)(~eq3)(L2 @ L4) | [append_functionality_wrt_list_iso] |
| Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L2(~eq2)L3 L1(~eq3)L3) | [list_iso_transitivity] |
| Thm* Discrete{T} (eq1,eq2:{T}, L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L) | [list_iso_inversion] |
| Thm* eq:{T}, L,M:T List. L(~eq)M M(~eq)L | [list_iso_commutative] |
| Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(~eq)M) | [list_iso_weakening_wrt_identity] |
| Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(~eq)(M @ L)) | [append_commutes_under_list_iso] |