T:Type, P:(T), L:(T List). l_all(filter(P; L); T; x.((P(x)))) 

latex

Definitions	t  T, P  Q, l_all(L; T; x.P(x)), x:A. B(x), P  Q, P  Q, prop{i:l}
Lemmas	bool wf, filter wf, l member wf, member filter