The idea is to have any i in any fin n, as long as n is 0 and i is j.
The catch used to be that i and j have different types, so cannot be compared using =. Hence ~...
Anyway, notice that in both branches of the induction, n gets instantiated to a successor, and hence the constraint on it is clearly false. A little (automated) bit of unification, and both these subgoals vanish vacuously. Pattern matching over fin 0 gives no cases.
Next: John Major equality | Prev: applying generic elim rules specifically | Up: contents