В следующем примере
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
postulate
f : Nat → Nat
g : ∀{x y} → f x ≡ suc y → Nat
h : Nat → Nat
h x with f x
h x | zero = zero
h x | suc y = g {x} {y} {!refl!}
Agda не принимает refl в качестве аргумента.
Основные вопросы:
- что я делаю не так?
- каков правильный / оптимальный / установленный / предпочтительный способ доказательства подобных вещей?
И, конечно, мы очень ценим любое понимание поведения Агды.