Level: Lib Thy Top: 1
Hypotheses:

  1. f :

  2. n :

  3. k :

  4. f n = f k

Conclusion:

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

Applied Tactic: BLemma `min_arg_unique` THEN Auto
Generated subgoals:

None