Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. l : n List

Conclusion:

en([]) < (n0)

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

None