Swapping out FMap with fin_maps from Std++.
Two remaining problems:
It would be nice if s and G were defined as Notations, rather than Definitions. This makes the Std++ tactics work much better and avoids having to use setoid_rewrite with all the map lemmas. Is there a way to make Ott generate Notation?
There is now a new admit in the type preservation proof – again there is a rewrite on maps that looks like it should unify but does not.
Swapping out
FMapwithfin_mapsfrom Std++. Two remaining problems:sandGwere defined as Notations, rather than Definitions. This makes the Std++ tactics work much better and avoids having to usesetoid_rewritewith all the map lemmas. Is there a way to make Ott generate Notation?admitin the type preservation proof – again there is a rewrite on maps that looks like it should unify but does not.