I think you want `Local Open Scope` for both of these, or else any file that `Require Import hit.epi` will be confused about having a different set of default scopes open.