Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. eq:T T . L:T List. xL.(x(eq) []) [] = L

Applied Tactic: UnivCD THENA Auto THEN D 0
Generated subgoals:

1. xL.(x(eq) []) [] = L

2. xL.(x(eq) []) [] = L