Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. l:n List. en(l) < (n||l||)

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

1. en([]) < (n0)

2. en(u::v) < (n||v|| + 1)