...
open import subtype Context as N

record Meta : Set where
  field
    context : Context
    c'      : Int
    next    : N.CodeSegment Context Context

open import subtype Meta as M
...