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