[Agda] Proof involving Fin

[Peter Thiemann]

Dear list,

I’m stuck with a proof involving the Fin module from the standard library.
I need to use Data.Fin.inject+ and the last definition is the lemma that I need.
However, when I try to solve the first hole by pattern matching on the argument of coerce list this:

inject+0n {suc n} zero with finn=n+0 n
... | p = {!!}

But then I cannot destruct p because its type is 
p : Fin n ≡ Fin (n + 0)

That ought to be fixable with a rewrite, but all alternatives I tried were rejected by Agda.

-Peter


%%%%%%%%%%%%
module Lemmas where

open import Data.Fin hiding (_+_ ; _≤_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality


-- about Fin and Nat
n=n+0 : (n : ℕ) → n ≡ n + 0
n=n+0 zero = refl
n=n+0 (suc n) = cong suc (n=n+0 n)

n+0=n : (n : ℕ) → n + 0 ≡ n
n+0=n zero = refl
n+0=n (suc n) = cong suc (n+0=n n)

m=n=>finm=finn : ∀ {m n : ℕ} → m ≡ n → Fin m ≡ Fin n
m=n=>finm=finn refl = refl

finn=n+0 : (n : ℕ) → Fin n ≡ Fin (n + 0)
finn=n+0 n = m=n=>finm=finn (n=n+0 n)

coerce : ∀ {A B : Set} → A ≡ B → A → B
coerce refl x = x

inject+0n : ∀ {n : ℕ} (fn : Fin n) → inject+ 0 fn ≡ coerce (finn=n+0 n) fn
inject+0n {zero} ()
inject+0n {suc n} zero = {!!}
inject+0n {suc n} (suc fn) = {!!}
%%%%%%%%%%%%