SizedTypesScopeViolationInMeta.agda:18,39-40
Cannot solve size constraints
[Id, k, m, j, n] j ≤ (_size_9 (i = j))
[Id, k, m, j, n] (↑ k) ≤ (_size_9 (i = k))
Reason: inconsistent lower bound for _size_9
when checking that the expression n has type Nat {_size_9 {i = j}}
