При написании этого ответа я заметил, что пока это работает как положено: onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat onlyModBy5 n = n foo : Nat foo = onlyModBy5 25 но как только я даю имя свойству, оно перестает...