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