Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. P : Alph List

  3. n:. (l:Alph List. ||l|| < n P l) (l:Alph List. ||l|| = n P l)

  4. l : Alph List

  5. n:. l:Alph List. ||l|| < n P l

Conclusion:

P l

Applied Tactic: With ||l|| + 1 (D 5) THENW Auto
Generated subgoals:

1. 0 ||l|| + 1

2. P l