[Agda] a version for Fin

[Sergei Meshveliani]

People,

This is about Fin and `lookup' of Standard library.

I am trying to prove the following simple lemma:

... (i : Fin (length xs)) → lookup xs i ≡ lookup (xs ++ [ y ]) i

Only the last occurrence of i needs to be replaced with
i' = (inject≀ i length-xs-≀-length-xs++y).

This proof occurs difficult for me.

Then I replace Fin with

Fin' : ℕ → Set
Fin' n = Σ ℕ (_< n)

And succeed with a proof for the corresponding lookup' and lemma'.

Is Fin' better?
Can people, please, provide a reasonably looking proof for `lemma' with
Fin ?

I attach a small source containing first the version (II) with Fin',
and then the formulation for version (I).

Thanks,

------
Sergei