AGDA_FAILURE

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