Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. R : T

  3. Fin(T) (t:T. Dec(R t))

Conclusion:

Dec(t:T. R t)

Applied Tactic: D 3
Generated subgoals:

1. Dec(t:T. R t)