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 D 0 THENW Auto THEN D 0 THENW Auto
Generated subgoals:

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

2. f n = f k