theory AEnv imports Arity Launchbury.Vars Launchbury.Env begin (* TODO: This could mostly be a Env-Nominal module *) type_synonym AEnv = "var ⇒ Arity⇩⊥" end