proposition: Lemma choose_upperbound_ineff'_close : forall xs ys x, choose_upperbound_ineff' xs ys = Some x -> List.In x ys.
proof: Proof. induction ys; intuition; try discriminate; simpl in *; remember (choose_upperbound_ineff' xs ys) as c; destruct c; [ right | destruct (check_upperbound_ineff a xs); inversion H ]; intuition. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General