Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. L:T List. || L 0

Applied Tactic: UnivCD THENA Auto THEN ListInd 2 THEN AbReduce 0
Generated subgoals:

1. 0 0

2. 1 + || v 0