P:(T
), L:T List. x
L.P(x) 
xL.P(x)L:T List, P:(T). xL.P(x) 
xL.P(x)eq:{T
}, P:(T), L:T List. 
xL.P(x) (
x:{x:T| x(eq) L }. P(x))
eq)(L,M) == xL.x(eq) MxL.P(x) == (letrec all L = (Case of L; nil 
true ; h.t P(h)
(all(t))) ) (L)
is mentioned by
| Thm* P:(T), L:T List. xL.P(x) xL.P(x) | [list_all_2_all] |
| Thm* L:T List, P:(T). xL.P(x) xL.P(x) | [list_all_iff_assert_list_all_2] |
| Thm* eq:{T}, P:(T), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) | [not_list_all_2_implies_exists_not] |
| Def (eq)(L,M) == xL.x(eq) M | [sublist_2] |