proposition: Lemma check_upperbound_ineff_sound : forall v xs, check_upperbound_ineff v xs = true -> upperbound v xs.
proof: Proof. unfold upperbound; induction xs; simpl in *; intuition; apply andb_true_iff in H; intuition; subst; find_if_inside; intuition. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General