Refined.Length

data Length p

type LengthEq n

type LengthMax n