eq:{T=
}, P:(T
Prop), L:T List. (
x:T. x(
eq) L & P(x)) 
yL.P(y)P:
. 
P P = falseP:. P P = true| Theorem | Name | ||
| Thm* eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y) | [list_exists_is_member_lemma] | ||
| cites | |||
| Thm* P:. P P = false | [not_assert_iff_bfalse] | ||
| Thm* P:. P P = true | [assert_iff_btrue] |