Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. n :

  3. n:. f:n Alph. Bij(n;Alph;f)

Conclusion:

n@0:. f:n@0 {l:Alph List| ||l|| = n} . Bij(n@0;{l:Alph List| ||l|| = n} ;f)

Applied Tactic: D 3 THEN D 4
Generated subgoals:

1. n@0:. f:n@0 {l:Alph List| ||l|| = n} . Bij(n@0;{l:Alph List| ||l|| = n} ;f)