(
eq1,eq2,eq3:{T
}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L2(~eq2)L3 L1(~eq3)L3) (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(
eq1)L2 L2(eq2)L3 L1(eq3)L3)| Rank | Theorem | Name | ||
| 3 | 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] | ||
| cites | ||||
| 2 | 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) | [sublist_transitivity] |