proposition: Theorem dumb_implementation : FullySharpened spec.
proof: Proof. start sharpening ADT. hone representation using dumbAbsRel; try queue. refine_testnil r_n. assert (r_o = nil) by eauto. subst. queue. refine_let (getLast r_n). erewrite dumbAbsRel_eta with (abs := r_o) by eauto. erewrite dumbAbsRel_pop_data by eauto. queue. cleanup. done. finalize. Defined.
imports: Tutorial