Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. B : T

  3. Fin(T)

  4. t:T. Dec(B t)

Conclusion:

Fin({t:T| B t} )

Applied Tactic: D 3
Generated subgoals:

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