agda - 任期が期待どおりに短縮されない

Answer 1

問題は、最初の式が にも使用できることですs+ ◃ y。がゼロではないことがわかった後でのみy、2 番目の方程式が適用されます。

解決策は簡単です：

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