Agda termination problem

Subst.Agda

subst-3m : ∀ k₁ k₂ k₃ es {Γ A B e e₁ j}
  → len es < k₁
  → size j < k₂
  → size-t B < k₃
  → Γ , A ⊢d j # e ▻ (es ⇈) ⦂ B
  → Γ ⊢d ♭ Z # e₁ ⦂ A
  → Γ ⊢d j # ((ƛ e) · e₁) ▻ es ⦂ B
subst-3m (suc k₁) (suc k₂) (suc k₃) [] sz₁ sz₂ sz₃ ⊢1 ⊢2 = ⊢d-app⇒ (⊢d-lam₂ ⊢1) ⊢2
subst-3m (suc k₁) (suc k₂) (suc k₃) (e ∷ es) {j = j} sz₁ sz₂ sz₃ ⊢1 ⊢2 =
  case lst-destruct-rev (e ∷ es) (ees>0 {e} {es}) of λ where
    ⟨ x , ⟨ xs , eq ⟩ ⟩ → case rw-apps→ {es = xs ⇈} (rw-try ⊢1 (eq-cons-↑ eq)) of λ where
                            (⊢d-app⇐ r r₁) → {!!}
                            (⊢d-app⇒ r r₁) → {!!}
                            (⊢d-sub {A = A} {B = B} ⊢e A≤B j≢Z) → case inspect j of λ where
                                                    (♭ Z with≡ j≡Z) → ⊥-elim (j≢Z j≡Z)
                                                    (♭ ∞ with≡ j≡∞) →
                                                          -- problematic function calls
                                                      let ind-e = subst-3m (suc k₁) k₂ ((suc (size-t B))) (xs ++ ⟦ x ⟧)
                                                                                       (sz-case₁ sz₁ eq) (sz-case₄ j≡∞ sz₂) {!!}
                                                                           ((rw-map {xs = xs} (rw-apps← {es = xs ⇈} ⊢e))) ⊢2
                                                      in ⊢d-sub' (rw-try' ind-e eq) A≤B
                                                    (♭ (S⇐ j') with≡ j≡Sj') → {!!}
                                                    (S⇒ i with≡ j≡Si) → {!!}
                            (⊢d-& {A = A} {B = B} ⊢e₁ ⊢e₂) →
                              let ind-e₁ = subst-3m (suc k₁) (suc k₂) k₃ (xs ++ ⟦ x ⟧) (sz-case₁ sz₁ eq) sz₂ (sz-case₂ {A = A} {B = B} sz₃)
                                                                   (rw-map {xs = xs} (rw-apps← {es = xs ⇈} ⊢e₁)) ⊢2
                                  ind-e₂ = subst-3m (suc k₁) (suc k₂) k₃ (xs ++ ⟦ x ⟧) (sz-case₁ sz₁ eq) sz₂ (sz-case₃ {A = A} {B = B} sz₃)
                                                                   (rw-map {xs = xs} (rw-apps← {es = xs ⇈} ⊢e₂)) ⊢2
                              in rw-try' (⊢d-& ind-e₁ ind-e₂) eq