Использование перезаписи внутри цели не верхнего уровня требует вспомогательной функции?

У меня есть формализация Agda-исчисления с индексами де Брейна. Большая часть настройки не имеет отношения к моей проблеме, поэтому я буду использовать пустые типы для переименований Ren и действий и просто постулирую базовое переименование sucᴿ, а также некоторые полезные операции и свойства переименований.

module Concur where

   open import Relation.Binary.PropositionalEquality
   -- de Bruijn indices:
   open import Data.Fin using () renaming (Fin to Name; module Fin to Name)
   open import Data.Nat as Nat using () renaming (ℕ to Cxt; module ℕ to Cxt)

   -- empty types will do here
   data Ren : Cxt → Cxt → Set where
   data Action (Γ : Cxt) : Set where

   postulate
      _∘_ : ∀ {Γ₁ Γ₂ Γ₃} → Ren Γ₂ Γ₃ → Ren Γ₁ Γ₂ → Ren Γ₁ Γ₃
      -- push a renaming under a binder
      suc : ∀ {Γ Γ′} → Ren Γ Γ′ → Ren (Cxt.suc Γ) (Cxt.suc Γ′)
      -- successor function on ℕ, qua renaming
      sucᴿ : ∀ {Γ} → Ren Γ (Cxt.suc Γ)
      -- apply a renaming to an action
      _*ᴬ_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Action Γ → Action Γ′
      -- here's a useful property
      suc-comm : ∀ {Γ Γ′} (ρ : Ren Γ Γ′) (a : Action Γ) → 
                 suc ρ *ᴬ (sucᴿ *ᴬ a) ≡ sucᴿ *ᴬ (ρ *ᴬ a)

Теперь я определю процессы, переходы и применение переименования к процессу, но ограничусь только двумя типами процессов и одним типом перехода.

   data Proc (Γ : Cxt) : Set where
      Ο : Proc Γ
      ν_ : Proc (Cxt.suc Γ) → Proc Γ

   data _—[_]→_ {Γ} : Proc Γ → Action Γ → Proc Γ → Set where
      ν_ : ∀ {P R} {a : Action Γ} → P —[ sucᴿ *ᴬ a ]→ R → ν P —[ a ]→ ν R

   infixl 0 _—[_]→_

   -- Apply a renaming to a process.
   _*_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Proc Γ → Proc Γ′
   ρ * Ο = Ο
   ρ * (ν P) = ν (suc ρ * P)

Вот моя проблема. Я хочу использовать свое полезное свойство suc-comm, чтобы показать, что я могу поднять произвольное переименование ρ на переход. В случае ν-binder это включает рекурсивный переход в подпереход E, использование suc для переименования под связкой и лемму suc-comm, чтобы показать, что вещи коммутируются правильно.

   -- A transition survives an arbitrary renaming.
   _*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
          P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
   ρ *¹ (ν_ {a = a} E) rewrite sym (suc-comm ρ a) =
      ν {!suc ρ *¹ E!} -- rewriting here doesn't help

К сожалению, как указано выше, использование rewrite для применения леммы не помогает, потому что цель не подходящего типа, пока я не попаду внутрь ν. Но я могу применять rewrite только на верхнем уровне тела функции. Так что мне, кажется, нужна вспомогательная функция, чтобы я мог rewrite в правильном контексте:

   _*²_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
          P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
   aux : ∀ {Γ Γ′ P R} (a : Action Γ) (ρ : Ren Γ Γ′) →
         P —[ sucᴿ *ᴬ a ]→ R → suc ρ * P —[ sucᴿ *ᴬ (ρ *ᴬ a) ]→ suc ρ * R
   ρ *² (ν_ {a = a} E) = ν aux a ρ E
   aux a ρ E rewrite sym (suc-comm ρ a) = suc ρ *² E

Это действительно работает, но кажется немного неудобным. Я что-то упустил? Есть ли способ избежать вспомогательной функции и как-то использовать лемму внутри предыдущей цели?