fact: Fixpoint check_upperbound_ineff (v : A) (xs : list A) : bool := match xs with | [ ] => true | x :: xs' => andb (if R_dec (f v) (f' x) then true else false) (check_upperbound_ineff v xs') end.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General