proposition: Theorem more_automated_dumb_implementation : FullySharpened spec.
proof: Proof. start sharpening ADT. hone representation using dumbAbsRel; try queue. refine_testnil r_n; [ queue | refine_let (getLast r_n); queue | ]. queue'. cleanup. done. finalize. Defined.
imports: Tutorial