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