eq:{T=
}, L,M:T List. L
(eq)M 
(
x:{x:T| x(
eq) L }. x(eq) M)P:
. P 
P = trueeq:{T=}, u:T. eq(u,u)| Theorem | Name | ||
| Thm* eq:{T=}, L,M:T List. L(eq)M (x:{x:T| x(eq) L }. x(eq) M) | [is_intersection_implies_exists_element] | ||
| cites | |||
| Thm* P:. P P = true | [assert_iff_btrue] | ||
| Thm* eq:{T=}, u:T. eq(u,u) | [discrete_equality_reflexive] |