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) (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* 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] | ||
| 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] |