Level: Lib Thy Top: 1
Hypotheses:

  1. f :

  2. n :

  3. i : (n + 1)

Conclusion:

MinAr(f;i;n) (i + 1)

Applied Tactic: NSubsetInd 3 THENA Auto' THEN RecCaseSplit `min_ar` THENA Auto'
Generated subgoals:

1. 0 1

2. MinAr(f;-1;n) 1

3. i (i + 1)

4. MinAr(f;i - 1;n) (i + 1)