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