coq - 一致から等しい証拠を抽出する

Question

私は次の作業をしようとしています:

    Definition gen `{A:Type}
           {i o: nat}
           (f: nat -> (option nat))
           {ibound: forall (n n':nat), f n = Some n' -> n' < i}
           (x: svector A i) (t:nat) (ti: t < o): option A
  := match (f t) with
     | None => None
     | Some t' => Vnth x (ibound t t' _)
     end.

最後の「_」の代わりに、「f t」が「Some t'」に等しいという証拠が必要です。試合からの入手方法がわかりませんでした。Vnth は次のように定義されます。

Vnth
     : ∀ (A : Type) (n : nat), vector A n → ∀ i : nat, i < n → A