[Agda] Dependent injection without K?

[Brandon Moore]

I am trying to prove something like fcinj in Coq. The code below compiles
normally, but is rejected with the --without-K flag. Is this sort of goal
provable without some sort of equality axiom?

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

data Fin : ℕ → Set where
  fz : ∀{n} → Fin (S n)
  fs : ∀{n} → Fin n → Fin (S n)

data FinCopy : ∀{n} → Fin n → Set where
  FZ : ∀{n} → FinCopy (fz {n})
  FS : ∀{n f} → FinCopy {n} f → FinCopy (fs f)

fcinj : ∀{n f} → FinCopy (fs {n} f) → FinCopy f
fcinj (FS y) = y