Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. n:
. Fin(Alph) 
Fin({l:Alph List| ||l|| = n} )
Applied Tactic: Unfold `finite` 0 THEN
UnivCD THENW Auto
Generated subgoals:1. 
n@0:. f:n@0 
{l:Alph List| ||l|| = n} . Bij(n@0;{l:Alph List| ||l|| = n} ;f)