Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. eq:{T=}. P:T . L:T List. x:T. x(eq) filter((x.P[x]);L) P[x]

Applied Tactic: UnivCD
Generated subgoals:

1. P[x]

2. x(eq) filter((x.P[x]);L)

3. T

4. T List

5. T

6. {T=}

7. '