proposition: Theorem SharpenedBookStore : FullySharpened BookStoreSpec.
proof: Proof. start sharpening ADT. start_honing_QueryStructure'. chooseIndexes. Focus 6. simpl in *. monad_simpl. Focused_refine_Query. implement_In_opt. distribute_filters_to_joins. implement_filters_using_find. monad_simpl. pick_new_database. finish honing. Focus 6. simpl in *. monad_simpl. Focused_refine_Query. implement_In_opt. distribute_filters_to_joins. implement_filters_using_find. monad_simpl. pick_new_database. finish honing. planOne. planOne. planOne. planOne. planOne. final_optimizations. determinize. choose_data_structures. final_simplification. use_this_one. Defined.
imports: Tutorial