This provides significant robustness against looping type class search.
As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:
Section fin_collection.
Context `{FinCollection A C}.
size_singleton (x : A) : size {[ x ]} = 1.
In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:
Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
In similar spirit, lemmas like the one below were also ambiguous:
Lemma lookup_alter_None {A} (f : A → A) m i j :
alter f i m !! j = None ↔ m !! j = None.
It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:
Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
alter f i m !! j = None ↔ m !! j = None.
That is, we have to specify the type of `m`.