Level: Lib Thy Top: 1
Hypotheses:

  1. P :

  2. n :

  3. k:{n...}. P k (i:k. P i)

  4. m :

  5. P m

Conclusion:

m:n. P m

Applied Tactic: Decide m < n THENW Auto
Generated subgoals:

1. m:n. P m

2. m:n. P m