proposition: Corollary choose_upperbound_ineff_is_upperbound : forall xs x, choose_upperbound_ineff xs = Some x -> upperbound x xs.
proof: Proof. unfold choose_upperbound_ineff; intuition; eapply choose_upperbound_ineff'_is_upperbound; eauto. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General