Level: Lib Thy Top: 1 1
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

Conclusion:

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

Applied Tactic: D 0 THENW Auto
Generated subgoals:

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