diff --git a/proof-libs/fstar/core/Core.Option.fst b/proof-libs/fstar/core/Core.Option.fst
index 08d8bed2d..d3c57c44a 100644
--- a/proof-libs/fstar/core/Core.Option.fst
+++ b/proof-libs/fstar/core/Core.Option.fst
@@ -7,6 +7,11 @@ let impl__and_then #t_Self #t (self: t_Option t_Self) (f: t_Self -> t_Option t):
   | Option_Some x -> f x
   | Option_None -> Option_None
 
+let impl__map #t_Self #t (self: t_Option t_Self) (f: t_Self -> t): t_Option t =
+  match self with
+  | Option_Some x -> Option_Some (f x)
+  | Option_None -> Option_None
+
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
 let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self