module Unsolved-meta-in-module-application where module M (A : Set) where open M _ public