proposition: Theorem refine_pick_upperbound_ineff : forall (xs : list A), refine (pick_upperbound xs) (ret (choose_upperbound_ineff xs)).
proof: Proof. unfold pick_upperbound, choose_upperbound_ineff; intuition; refine pick val _; try reflexivity; intuition; [ apply choose_upperbound_ineff_close | apply choose_upperbound_ineff_is_upperbound ]; trivial. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General