fact: Fixpoint choose_upperbound_ineff' (xs : list A) (ys : list A) : option A := match ys with | [ ] => None | y :: ys' => match choose_upperbound_ineff' xs ys' with | None => if check_upperbound_ineff y xs then Some y else None | Some v => Some v end end.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General