如何解决Cubical Agda中M类型相关的非终止错误？

record M (S : Set) (Q : S → Set) : Set where
  coinductive
  constructor sup-M
  field
    shape : S
    pos : Q shape → M S Q
open M

我定义了基于M的族Pos，其目标类型限定为sup-M构造的形式，而非任意M类型值：

data Pos : M S Q → Set where
    here : {s : S} {f : Q s → M S Q} → Pos (sup-M s f) 
    below : {s : S} {f : Q s → M S Q} → (q : Q s) → Pos (f q) → Pos (sup-M s f)

针对固定的S : Set、Q : S → Set、X Y : Set、s : S、h : Q s → Y、g : Y → X，我定义了从Y到M S Q的函数β₁：

β₁ : Y → M S Q
shape (β₁ y) = s
pos (β₁ y) = β₁ ∘ h

当我试图定义函数β₂ : (y : Y) → Pos (β₁ y) → X时，无法直接对第二个参数做模式匹配——因为它的类型不是Pos (sup-M s f)的形式。

我借助Cubical Agda中M类型的命题性eta等式绕开这个问题：

M-eta-eq : {S : Set} {Q : S → Set} (m : M S Q) → sup-M (shape m) (pos m) ≡ m
shape (M-eta-eq m i) = shape m
pos (M-eta-eq m i) = pos m

于是我先定义辅助函数β₂'，它的参数类型是Pos (sup-M s (β₁ ∘ h))，支持直接模式匹配；再通过M-eta-eq将β₁ y与sup-M s (β₁ ∘ h)的等价性来定义β₂：

β₂' : (y : Y) → Pos (sup-M s (β₁ ∘ h)) → X
β₂' y here = g y
β₂' y (below q p) = β₂' (h q) (subst Pos (sym (M-eta-eq (β₁ (h q)))) p)

β₂ : (y : Y) → Pos (β₁ y) → X
β₂ y p = β₂' y (subst Pos (sym (M-eta-eq (β₁ y))) p)

但这段代码触发了非终止错误，推测是因为Agda无法识别subst Pos (sym (M-eta-eq (β₁ (h q)))) p在结构上小于below q p。

能否向Agda证明β₂'是终止的？或许可以借助subst-filler实现？

我尝试过其他方法：比如用Pos的消除子定义β₂，或者在Pos的构造函数中添加m ≡ sup-M s f形式的等式，让目标类型为Pos m。这两种方法都成功定义了β₂，但后续涉及β₂的等式证明会引入大量subst和transport操作，非常繁琐。

想请教是否有更优的Pos族定义方式，尤其考虑到Cubical Agda对归纳族的支持尚未完善。

内容的提问来源于stack exchange，提问作者sigma