Level: Lib Thy Top: 2
Hypotheses:

  1. n :

  2. l : n List

  3. u : n

  4. v : n List

  5. en(v) < (n||v||)

Conclusion:

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

Applied Tactic: RecUnfold `en` 0 THEN Reduce 0
Generated subgoals:

1. u + en(v) * n < (n||v|| + 1)