Termination checking failed for the following functions: cut⁺, cut⁻, rsubst+, lsubst Problematic calls: cut⁺ (conssusp pfΓ) pf LA (wken-all-rfoc Values) N (at Issue1075.agda:337,40-44) rsubst+ [] pfΓ pf LA (A ∷ []) (N ∷ []) Values N' (at Issue1075.agda:339,3-10) cut⁺ pfΓ pf (B ∷ LA) (V₂ ∷ Values) (cut⁺ pfΓ pf (A ∷ []) (V₁ ∷ []) N) (at Issue1075.agda:344,60-64) cut⁺ pfΓ pf (A ∷ []) (V₁ ∷ []) N (at Issue1075.agda:344,96-100) lsubst pfΓ pf N₁ N₂ (at Issue1075.agda:359,60-66) cut⁺ pfΓ (record {}) (x ∷ []) (V ∷ []) N₁ (at Issue1075.agda:362,32-36) cut⁻ pfΓ (pf₁ , pf) (A ∷ []) refl (?0 Γ' LA- x x₁ pfΓ pf LT pf₁ Sp) (rsubst-v Γ' pfΓ pf LA- LT Sp ∷ []) (at Issue1075.agda:381,3-7) cut⁺ pfΓ (proj₂ pf) (A ∷ []) (V ∷ []) N (at Issue1075.agda:429,32-36)