feat(ext): ext fails if it can't make progress

[semorrison]

Per discussion with @cipher1024 on zulip.

[cipher1024]

Is there any test case for under test/ for ext? It's not a rule of mathlib but I find it a useful thing to keep. In change sets, that already gives you a diff on how the use of the tactic will change or at least just an example use of the tactic.

[semorrison]

There were test cases for ext1. I added two more test cases, checking that ext behaves as expected when there are either 2 or 0 levels of extensionality lemmas to apply.

[semorrison]

Closing this, as @cipher1024 has included this functionality in his more recent PR 3a4dd38, including test cases.