eq:{T=
}, x,y:T, L:T List. x(
eq) L 
eq(x,y) x(eq) remove(eq;y;L)P:
. P 
P = trueT:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq T
T| Theorem | Name | ||
| Thm* eq:{T=}, x,y:T, L:T List. x(eq) L eq(x,y) x(eq) remove(eq;y;L) | [not_is_member_remove_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] |