diff --git a/src/core/Core.ml b/src/core/Core.ml
index bc001315b..954cbde3a 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -497,6 +497,12 @@ let (?|) gs st =
 
 let conde = (?|)
 
+let condo2 a b st =
+  let st = State.new_scope st in
+  match Stream.msplit @@ a st with
+  | Some (a, b) -> Stream.cons a b
+  | None -> b st
+
 let call_fresh f st =
   let x = State.fresh st in
   f x st
diff --git a/src/core/Core.mli b/src/core/Core.mli
index 7f2612b24..fff880bc9 100644
--- a/src/core/Core.mli
+++ b/src/core/Core.mli
@@ -82,6 +82,8 @@ val (|||) : goal -> goal -> goal
 *)
 val (?|) : goal list -> goal
 
+val condo2 : goal -> goal -> goal
+
 (** [conde] is a synonym for [?|] *)
 val conde : goal list -> goal