{α : Type u_1} →
  {ε : Type u_2} →
    [inst : Preorder α] →
      (a : Thunk α) →
        (α → Bool) →
          [inst_1 : Estimator a ε] →
            [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] → (_ : ε) ×' Bool → Except (Option ε) ε