Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
R:T
. Fin(T)
(
t:T. Dec(R t))
Dec(
t:T. R t)
Applied Tactic:
GenUnivCD THENW Auto
Generated subgoals:
1
. Dec(
t:T. R t)
T:
. R:T 
. Fin(T) 
(t:T. Dec(R t)) 
Dec(
t:T. R t)t:T. R t)