Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. P l