equality - “subst”，其中要等同的索引也使用 subst

Question

我坚持以下。我推导了在某些上下文 Γ 中发生的 pi 演算转换，以及 Γ ≡ Γ' 的证明。我想将推导强制转换为 Γ' 中的转换，使用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 很容易。问题是转换的目标 R，其类型取决于 a。在强制转换中，我使用subst将 a 从 Γ ⟿ 强制转换为 Γ' ⟿。天真地，我还想通过显示 Proc 索引相等来subst将 R 的类型从 更改为。但是，就其本质而言，它与 a 具有不同的类型，因此我不确定如何执行此操作。也许我需要再次使用 Γ ≡ Γ′ 的证明，或者以某种方式“撤消”内部来统一类型。Proc (target a)Proc (target (subst _⟿ q a)subst _⟿ q asubst

我想做的事合理吗？如果是这样，鉴于异质性，我如何强制 R？

Answer 1