Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
f:T
.
L:T List. filter(f;L)
{x:T|
(f x)} List
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. filter(f;L)
{x:T|
(f x)} List
T:
. f:T 
. L:T List. filter(f;L) 
{x:T| 
(f x)} List {x:T| (f x)} List