diff --git a/src/std/List.ml b/src/std/List.ml
index 8ac967c35..afd2c529d 100644
--- a/src/std/List.ml
+++ b/src/std/List.ml
@@ -94,6 +94,7 @@ let reify_list   = reify
 let list_reify = reify
 let prj_exn_list = prj_exn
 let list_prj_exn = prj_exn
+let ground_prj_exn = prj_exn
 
 (* let rec prj : (int -> _ ground) -> ('a, 'b) Reifier.t -> ('a groundi, 'b ground) Reifier.t =
   fun onvar ra ->
diff --git a/src/std/List.mli b/src/std/List.mli
index 00830ea2a..1904f3912 100644
--- a/src/std/List.mli
+++ b/src/std/List.mli
@@ -102,6 +102,8 @@ val prj_exn : ('a, 'b) Reifier.t -> ('a injected, 'b ground) Reifier.t
 (** [list_prj_exn] is a synonym for [prj_exn] *)
 val list_prj_exn : ('a, 'b) Reifier.t -> ('a injected, 'b ground) Reifier.t
 
+val ground_prj_exn : ('a, 'b) Reifier.t -> ('a injected, 'b ground) Reifier.t
+
 (** Synonyms to comply with the generic naming scheme *)
 val reify_list   : ('a, 'b) Reifier.t -> ('a injected, 'b logic) Reifier.t
 
diff --git a/src/std/Option.mli b/src/std/Option.mli
index e77c19a36..e5afbc4f8 100644
--- a/src/std/Option.mli
+++ b/src/std/Option.mli
@@ -33,10 +33,10 @@ open Core
 (** Logic option *)
 @type 'a logic = 'a GT.option Logic.logic with show, gmap, html, eq, compare, foldl, foldr, fmt
 
-(** Type synonyms to comply with the generic naming scheme *)                                             
+(** Type synonyms to comply with the generic naming scheme *)
 @type 'a option       = 'a ground with show, gmap, html, eq, compare, foldl, foldr, fmt
 @type 'a option_logic = 'a logic with show, gmap, html, eq, compare, foldl, foldr, fmt
-                                             
+
 (** {2 Relational API} *)
 
 (** Logic injection (for reification) *)
@@ -58,10 +58,10 @@ val reify : ('a, 'b) Reifier.t -> ('a injected, 'b logic) Reifier.t
 (* Shallow non-variable projection *)
 val prj_exn : ('a, 'b) Reifier.t -> ('a injected, 'b ground) Reifier.t
 
-(** Synonyms to comply with the generic naming scheme *)                                             
+(** Synonyms to comply with the generic naming scheme *)
 val reify_option   : ('a, 'b) Reifier.t -> ('a injected, 'b logic) Reifier.t
 val prj_exn_option : ('a, 'b) Reifier.t -> ('a injected, 'b ground) Reifier.t
-  
+
 (** {3 Constructors} *)
 
 (** Logic dual of constructor [Some] from {!Stdlib.Option}. *)