A : Type
  i : nat
  index_f : nat → nat
  n : nat
  ip : n < i
  partial_index_f : nat → option nat
  L : partial_index_f (index_f n) ≡ Some n
  V : ∀ i0 : nat, i0 < i → option A
  l : ∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i
  ============================
   V n ip
   ≡ match
       partial_index_f (index_f n) as fn
       return (partial_index_f (index_f n) ≡ fn → option A)
     with
     | Some z => λ p : partial_index_f (index_f n) ≡ Some z, V z (l z p)
     | None => λ _ : partial_index_f (index_f n) ≡ None, None
     end eq_refl

Error: Abstracting over the term "partial_index_f (index_f n)"
leads to a term
"λ o : option nat,
 V n ip
 ≡ match o as fn return (o ≡ fn → option A) with
   | Some z => λ p : o ≡ Some z, V z (l z p)
   | None => λ _ : o ≡ None, None
   end eq_refl" which is ill-typed.

destruct (partial_index_f (index_f n)).
  inversion L.
  generalize (l n0 eq_refl).
  intros. subst n0.
  replace l0 with ip by apply proof_irrelevance.
  reflexivity.
  congruence.