[Agda] --without-K option too restrictive?

[Andrés Sicard-Ramírez]

Hi,

As far as I understand, the --without-K option rejects the K-rule which
cannot be proved using subst. Given

open import Data.List
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Relation.Binary
module NDTO = DecTotalOrder decTotalOrder

P : {A : Set} → List A → List A → Set
P xs ys = ∃ (λ x → ys ≡ x ∷ xs)

Q : {A : Set} → List A → List A → Set
Q xs ys = (length xs) < (length ys)

helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))
helper y []       = s≤s z≤n
helper y (x ∷ xs) = s≤s NDTO.refl

Why the --without-K option rejects the following proof

foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo xs .(x ∷ xs) (x , refl) = helper x xs

if I can prove foo using only subst

foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo' xs ys (x , h) =
  subst (λ ys' → length xs < length ys') (sym h) (helper x xs)

?

Thanks,

-- 
Andrés