eq:{T=
}, x:T, L,M:T List. x(
eq) L 
L(
eq)M x(eq) MP:
. P 
P = trueT:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq T
T| Theorem | Name | ||
| Thm* eq:{T=}, x:T, L,M:T List. x(eq) L L(eq)M x(eq) M | [is_member_sublist_lemma] | ||
| cites | |||
| Thm* P:. P P = true | [assert_iff_btrue] | ||
| Thm* T:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT | [discrete_equality_properties] |