[Agda] Need a hand with a proof

[Jacques Carette]

Self-contained code with one hole.  The main theorem 'List A ↔ Σ ℕ (Vec 
A)' ought to be obvious. Certainly the two functions that witness it 
are; the problem is to prove left-inverse. The right-inverse is already 
in Data.Vec.Properties. I've tried many ideas, to no avail.

Jacques

module help where

open import Data.List using (List; _∷_; []; length)
open import Data.Vec using (Vec; _∷_; []; fromList; toList)
open import Data.Vec.Properties using (toList∘fromList; ∷-injective)
open import Data.Product using (Σ; _,_; proj₁; proj₂)

open import Function using (_∘_; _↔_; _$_)

open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; subst; cong; sym; trans)

private
   variable
     a : Level
     A : Set a

forgetting-length : {a : Level} {A : Set a} → List A ↔ Σ ℕ (Vec A)
forgetting-length = record
   { f = λ xs → length xs , fromList xs
   ; f⁻¹ = toList ∘ proj₂
   ; cong₁ = λ { refl → refl }
   ; cong₂ = λ { refl → refl }
   ; inverse = left-inv , toList∘fromList
   }
   where
     length-stable : (x : Σ ℕ (Vec A)) → length (toList (proj₂ x)) ≡ proj₁ x
     length-stable (0 , []) = refl
     length-stable (suc i , x ∷ xs) = cong suc (length-stable (i , xs))

     left-inv : (x : Σ ℕ (Vec A)) → (length (toList (proj₂ x)) , 
fromList (toList (proj₂ x))) ≡ x
     left-inv (0 , []) = refl
     left-inv (suc n , x ∷ xs) = {!!}