Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

S,T:. Fin(S) Fin(T) Fin(S T)

Applied Tactic: Unfold `finite` 0
Generated subgoals:

1. S,T:. (n:. f:n S. Bij(n;S;f)) (n:. f:n T. Bij(n;T;f)) (n:. f:n S T. Bij(n;S T;f))