turns out we can import with shorter names (and we actually already do that frequently in "From Coq Import")