期望一个无关紧要的论点，但发现了一个相关的论点

Question

在以下程序中，我想递归定义fsplit'：

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Fin
open import Cubical.Data.Sum

lemma : ∀ {x y} → x + suc y ≡ 1 → 0 ≡ y
lemma {x = x} {y = y} p = sym (snd (m+n≡0→m≡0×n≡0 {x} {y} (cong predℕ (sym (+-suc x y) ∙ p))))

fsplit′ : ∀ {k} (fj : Fin (suc k))
  → (flast ≡ fj) ⊎ (Σ[ fk ∈ Fin k ] inject< ≤-refl fk ≡ fj)
fsplit′ {k = zero} (j , fst₁ , p) = inl (Fin-fst-≡ (lemma p))
fsplit′ {k = suc k} (0 , q) = inr (0 , Fin-fst-≡ refl)
fsplit′ {k = suc k} (suc j , q) with fsplit′ {k = k} (j , pred-≤-pred q)
... | _ = ?

我的目的是根据递归呼叫的结果进行模式匹配fsplit'{k = k}（j，j，pret-- ≤预先Q）。但是，使用构造的将导致AGDA 2.6.2.2的以下错误消息：

Expected an irrelevant argument, but found a relevant argument
when checking that the type
(k j : ℕ) (q : suc j < suc (suc k)) →
((k ,
  0 ,
  (λ i →
     suc
     (hcomp
      (λ i₁ .o →
         Agda.Builtin.Nat.suc-0
         (primPOr i (~ i) (λ .o₁ → suc k) (λ .o₁ → suc k) o))
      k)))
 ≡
 (j ,
  fst q ,
  (λ i →
     predℕ
     (hcomp (doubleComp-faces (λ _ → suc (fst q + suc j)) (snd q) i)
      (+-suc (fst q) (suc j) (~ i))))))
⊎
Σ (Σ ℕ (λ k₁ → Σ ℕ (λ k₂ → k₂ + suc k₁ ≡ k)))
(λ fk →
   (fst fk ,
    suc (fst (snd fk) + 0) ,
    (λ i →
       suc
       (hcomp
        (λ i₁ .o →
           Agda.Builtin.Nat.suc-0
           (primPOr i (~ i)
            (λ .o₁ →
               suc
               (hcomp
                (λ i₂ .o₂ →
                   Agda.Builtin.Nat.suc-0
                   (primPOr i₁ (~ i₁) (λ .o₃ → suc k)
                    (λ .o₃ → suc (fst (snd fk) + suc (fst fk))) o₂))
                (hcomp
                 (λ i₂ .o₂ →
                    Agda.Builtin.Nat.suc-0
                    (primPOr i₁ (~ i₁)
                     (λ .o₃ →
                        suc
                        (hcomp
                         (λ i₃ .o₄ →
                            Agda.Builtin.Nat.suc-0
                            (primPOr i₂ (~ i₂)
                             (λ .o₅ →
                                suc
                                (hcomp
                                 (doubleComp-faces (λ _ → suc (fst (snd fk) + fst fk))
                                  (snd (snd fk)) i₃)
                                 (+-suc (fst (snd fk)) (fst fk) (~ i₃))))
                             (λ .o₅ → suc (fst (snd fk) + suc (fst fk))) o₄))
                         (+-suc (fst (snd fk)) (fst fk) i₂)))
                     (λ .o₃ → suc (fst (snd fk) + suc (fst fk))) o₂))
                 (fst (snd fk) + suc (fst fk)))))
            (λ .o₁ → suc (fst (snd fk) + 0 + suc (fst fk))) o))
        (+-zero (fst (snd fk)) i + suc (fst fk)))))
   ≡
   (j ,
    fst q ,
    (λ i →
       predℕ
       (hcomp (doubleComp-faces (λ _ → suc (fst q + suc j)) (snd q) i)
        (+-suc (fst q) (suc j) (~ i)))))) →
((suc k ,
  0 ,
  (λ i →
     suc
     (suc
      (hcomp
       (λ i₁ .o →
          Agda.Builtin.Nat.suc-0
          (primPOr i (~ i) (λ .o₁ → suc k) (λ .o₁ → suc k) o))
       k))))
 ≡ (suc j , q))
⊎
Σ (Σ ℕ (λ k₁ → Σ ℕ (λ k₂ → k₂ + suc k₁ ≡ suc k)))
(λ fk →
   (fst fk ,
    suc (fst (snd fk) + 0) ,
    (λ i →
       suc
       (hcomp
        (λ i₁ .o →
           Agda.Builtin.Nat.suc-0
           (primPOr i (~ i)
            (λ .o₁ →
               suc
               (hcomp
                (λ i₂ .o₂ →
                   Agda.Builtin.Nat.suc-0
                   (primPOr i₁ (~ i₁) (λ .o₃ → suc (suc k))
                    (λ .o₃ → suc (fst (snd fk) + suc (fst fk))) o₂))
                (hcomp
                 (λ i₂ .o₂ →
                    Agda.Builtin.Nat.suc-0
                    (primPOr i₁ (~ i₁)
                     (λ .o₃ →
                        suc
                        (hcomp
                         (λ i₃ .o₄ →
                            Agda.Builtin.Nat.suc-0
                            (primPOr i₂ (~ i₂)
                             (λ .o₅ →
                                suc
                                (hcomp
                                 (doubleComp-faces (λ _ → suc (fst (snd fk) + fst fk))
                                  (snd (snd fk)) i₃)
                                 (+-suc (fst (snd fk)) (fst fk) (~ i₃))))
                             (λ .o₅ → suc (fst (snd fk) + suc (fst fk))) o₄))
                         (+-suc (fst (snd fk)) (fst fk) i₂)))
                     (λ .o₃ → suc (fst (snd fk) + suc (fst fk))) o₂))
                 (fst (snd fk) + suc (fst fk)))))
            (λ .o₁ → suc (fst (snd fk) + 0 + suc (fst fk))) o))
        (+-zero (fst (snd fk)) i + suc (fst fk)))))
   ≡ (suc j , q))
of the generated with function is well-formed

这里发生了什么？我如何在fsplit'的定义中进行反复分支？