module Error-in-imported-module where

open import Error-in-imported-module.M