diff --git a/proofs/agda/EchoBitNarrowingNumeric.agda b/proofs/agda/EchoBitNarrowingNumeric.agda
index 3d1621f..c193149 100644
--- a/proofs/agda/EchoBitNarrowingNumeric.agda
+++ b/proofs/agda/EchoBitNarrowingNumeric.agda
@@ -7,7 +7,7 @@
 module EchoBitNarrowingNumeric where
 
 open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_; _<_; _≤_; z≤n; s≤s)
-open import Data.Nat.Properties using (+-suc; +-identityʳ; *-assoc; ≤-step)
+open import Data.Nat.Properties using (+-suc; +-identityʳ; *-assoc; m≤n⇒m≤1+n)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; sym; trans; subst; module ≡-Reasoning)
@@ -48,7 +48,7 @@ private
   double-mono (s≤s p) = s≤s (s≤s (double-mono p))
 
   join-bound : ∀ {m n} → m < n → ∀ b → joinBit m b < double n
-  join-bound (s≤s p) O = s≤s (≤-step (double-mono p))
+  join-bound (s≤s p) O = s≤s (m≤n⇒m≤1+n (double-mono p))
   join-bound (s≤s p) I = s≤s (s≤s (double-mono p))
 
 -- The bit-vector reconstruction has the exact arithmetic shape of the API.
diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda
index b1e6fba..95fcc90 100644
--- a/proofs/agda/EchoExampleParser.agda
+++ b/proofs/agda/EchoExampleParser.agda
@@ -78,11 +78,14 @@ paren-pair = LP ∷ RP ∷ LP ∷ RP ∷ []
 -- The auxiliary's signature `ℕ → List Token → Bool` mirrors a state
 -- machine. We pattern-match on the token first (Agda-friendly recursion
 -- shape) and on the depth only in the RP case (the abort condition).
+-- The LP clause comes first so the case tree splits on the token
+-- before the depth: every clause then holds definitionally, which
+-- `--exact-split` requires.
 
 parses-aux : ℕ → List Token → Bool
+parses-aux d       (LP ∷ ts)  = parses-aux (suc d) ts
 parses-aux zero    []         = true
 parses-aux (suc _) []         = false
-parses-aux d       (LP ∷ ts)  = parses-aux (suc d) ts
 parses-aux zero    (RP ∷ _)   = false
 parses-aux (suc d) (RP ∷ ts)  = parses-aux d ts
 
@@ -111,7 +114,8 @@ paren-nested≢paren-pair p =
   where
     second-token : List Token → Token
     second-token (_ ∷ t ∷ _) = t
-    second-token _           = LP   -- default; never reached for these inputs
+    second-token []          = LP   -- default; never reached for these inputs
+    second-token (_ ∷ [])    = LP
 
 paren-empty≢paren-nested : paren-empty ≢ paren-nested
 paren-empty≢paren-nested p =
diff --git a/proofs/agda/EchoTropical.agda b/proofs/agda/EchoTropical.agda
index 72fc148..fd89672 100644
--- a/proofs/agda/EchoTropical.agda
+++ b/proofs/agda/EchoTropical.agda
@@ -24,7 +24,7 @@ infixl 6 _⊕_
 
 _⊕_ : ℕ → ℕ → ℕ
 zero ⊕ n = n
-m ⊕ zero = m
+suc m ⊕ zero = suc m
 suc m ⊕ suc n = suc (m ⊕ n)
 
 -- Basic tropical properties (simplified for bridge purposes)