[Agda] subst puzzle

[Jacques Carette]

Here is a self-contained puzzle that has me stumped. I'm sure there are 
lemmas in Relation.Binary.PropositionalEquality.Properties that ought to 
apply, but I just can't see it.  Ideas?

Jacques

module Puzzle where

open import Data.Nat using (ℕ; _+_; zero)
open import Data.Fin using (Fin; splitAt)
open import Relation.Binary.PropositionalEquality using (_≡_; subst)
open import Data.Sum using (inj₁)

lemma : (k : ℕ) (m : Fin k) (p : k ≡ k + 0) → splitAt k (subst Fin p m) 
≡ inj₁ m
lemma k m p = {!!}