pattern-matching - 定理からの情報を使用したパターン マッチング

Question

次の質問があります。コードを見てください。

  (* Suppose we have type A *)
  Variable A: Type.

  (* Also we have a function that returns the type (option A) *)
  Definition f_opt x: option A := ...

  (* Then, I can prove that this function always returns something: *)
  Theorem always_some: forall x, exists y, f_opt x = Some y.
  Admitted.

  (* Or, equivalently: *)
  Theorem always_not_none: forall x, f_opt x <> None.
  Admitted.

f_optここで、常に type の値を返すバージョンを取得したいと思いますA。このようなもの：

  Definition f x: A :=
    match f_opt x with
      | Some y => y
    end.

しかし、次のエラーが表示されます。

非網羅的なパターン マッチング: pattern の句が見つかりませんNone。

型で何らかの作業を行う必要があることは理解していますが、正確に何をすべきかわかりません。