fact: Definition pick_upperbound (xs : list A) : Comp (option A) := {x | (forall x', x = Some x' -> List.In x' xs /\ upperbound x' xs)}%comp.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General