eq:{T=
}, P:(T
Type), L:T List. x
L.P(x) 
(x:{x:T| x(eq) L }. P(x))eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L 
P(z))P:
. P P = true| Rank | Theorem | Name | ||
| 2 | Thm* eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) | [list_all_all] | ||
| cites | ||||
| 1 | Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) | [list_all_is_member_lemma] | ||
| 0 | Thm* P:. P P = true | [assert_iff_btrue] |