Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. P:T . L,M:T List. filter((x.P[x]);(L @ M)) = filter((x.P[x]);L) @ filter((x.P[x]);M)

Applied Tactic: UnivCD THENA Auto THEN Fiat
Generated subgoals:

None