Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. B : T

  3. n :

  4. f:n T. Bij(n;T;f)

  5. t:T. Dec(B t)

Conclusion:

Fin({t:T| B t} )

Applied Tactic: (InstLemma `fin_dec_fin` [n;T; B] ...a)
Generated subgoals:

1. 1-1-Corresp(n;T)

2. Fin({t:T| B t} )