Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. R : T

  3. Fin(T)

  4. t:T. Dec(R t)

Conclusion:

Dec(t:T. R t)

Applied Tactic: Assert n:. T:. R:T . (f:n T. Bij(n;T;f)) (t:T. Dec(R t)) Dec(t:T. R t)
Generated subgoals:

1. n:. T:. R:T . (f:n T. Bij(n;T;f)) (t:T. Dec(R t)) Dec(t:T. R t)

2. Dec(t:T. R t)