eq:{T=
}, P:(T
Type), L:T List. 
x
L.P(x) 
(x:{x:T| x(eq) L }. P(x))P:
. 
P P = falseP:. P P = true| Theorem | Name | ||
| Thm* eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) | [list_exists_exists] | ||
| cites | |||
| Thm* P:. P P = false | [not_assert_iff_bfalse] | ||
| Thm* P:. P P = true | [assert_iff_btrue] |