Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. n :

  3. n1 :

  4. f : n1 Alph

  5. Bij(n1;Alph;f)

Conclusion:

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

Applied Tactic: With (n1n) (D 0) THENA Auto
Generated subgoals:

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