Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
B:T
. Fin(T)
(
t:T. Dec(B t))
Fin({t:T| B t} )
Applied Tactic:
(GenRepD ...a)
Generated subgoals:
1
. Fin({t:T| B t} )
T:
. B:T 
. Fin(T) 
(t:T. Dec(B t)) 
Fin({t:T| B t} )