Next: John Major equality | Prev: applying generic elim rules specifically | Up: contents


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


Conor's Work Page