HomeIsabelle/Phabricator

more accurate export morphism enables proper instantiation by interpretation