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)eq:{T}, L,M:T List, x:T. x(
eq) (L @ M) 
x(eq) L 
x(eq) M| Theorem | Name | ||
| 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_sublist] | ||
| cites | |||
| Thm* eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) L x(eq) M | [is_member_of_append_lemma] |