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

P l

Applied Tactic: Assert n:. l:Alph List. ||l|| < n P l
Generated subgoals:

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

2. P l