Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

f: . n,k:. f n = f k MinArg(f : {0..n}) = MinArg(f : {0..k})

Applied Tactic: UnivCD THENW Auto THEN Unfold `min_arg` 0
Generated subgoals:

1. n - MinAr(f;n;n) = k - MinAr(f;k;k)