agda - 期限未按预期减少

Answer 1

The problem is that the first equation can also be used for s+ ◃ y. Only after you know that y is not zero, the second equation applies.

The solution is simple:

lemma : ∀ y  → s+ ◃ y ≡ + y
lemma zero    = refl
lemma (suc _) = refl