feat: implement `ext?` and `ext!?`

[joneugster]

Implement ext?, ext1? to show used extensionality lemmas, and ext!? to brute-force try all ext-lemmas.

• ext? displays a tactic replacement suggestion that could replace the ext. The tactic sequence comprises the tactics apply, intros, and sorry.
• ext!? ignores the type in the DiscrTree and goes through all lemmas but yields a warning when it applied a lemma that had the wrong type, suggesting to add a copy of the lemma to the library.

[joneugster]

I think now I'm happy with the functionality and it should be ready for a review.