equality - 同等化されるインデックスも subst を使用する「subst」

Question

私は次のことで立ち往生しています。私は、ある文脈Γで起こるパイ微積分遷移の導出と、Γ ≡ Γ' の証明を持っています。を使用して、導関数を Γ' の遷移に強制したいと思いsubstます。いつものように、設定の詳細はほとんど重要ではありません。

module Temp where
   open import Data.Nat as Nat using (_+_) renaming (ℕ to Cxt)
   open import Function
   open import Relation.Binary.PropositionalEquality

   data _⟿ (Γ : Cxt) : Set where
      bound : Γ ⟿
      nonBound : Γ ⟿

   target : ∀ {Γ} → Γ ⟿ → Cxt
   target {Γ} bound = Γ + 1
   target {Γ} nonBound = Γ

   data Proc (Γ : Cxt) : Set where
   data _—[_]→_ {Γ} : Proc Γ → (a : Γ ⟿) → Proc (target a) → Set where

   -- Use a proof that Γ ≡ Γ′ to coerce a transition in Γ to one in Γ'.
   coerce : ∀ {Γ Γ′} {P : Proc Γ} {a R} → P —[ a ]→ R → (q : Γ ≡ Γ′) →
               subst Proc q P —[ subst _⟿ q a ]→ subst (Proc ∘ target) {!!} R
   coerce E refl = {!!}

トランジションのソース P と、トランジションのラベルとして表示されるアクション a の両方を強制するのは簡単です。問題は、型が a に依存する遷移のターゲット R です。強制遷移では、substa を Γ ⟿ から Γ' ⟿ に強制するために使用します。単純に、Proc インデックスが等しいことを示すことで、 R の型を からにsubst変更するためにも使用したいと思います。ただし、その性質上、 a とは異なる型を持っているため、これを行う方法がわかりません。たぶん、Γ ≡ Γ′ の証明をもう一度使うか、型を統一するために内側を「元に戻す」必要があるかもしれません。Proc (target a)Proc (target (subst _⟿ q a)subst _⟿ q asubst

私がやろうとしていることは合理的ですか？もしそうなら、異質性を考慮してRを強制するにはどうすればよいですか?