The attribute indexes extensionality lemma using the type of the
objects (i.e. my_collection) which it gets from the statement of
the lemma. In some cases, the same lemma can be used to state the
extensionality of multiple types that are definitionally equivalent.
ext1 id selects and apply one extensionality lemma (with attribute
ext), using id, if provided, to name a local constant
introduced by the lemma. If id is omitted, the local constant is
named automatically, as per intro. Placing a ? after ext1
(e.g. ext1? i ⟨a,b⟩ : 3) will display a sequence of tactic
applications that can replace the call to ext1.