proposition: Theorem even_more_automated_implementation : FullySharpened spec.
proof: Proof. start sharpening ADT. hone representation using absRel; try queue. refine_testnil (fst r_n); [ refine_testnil (snd r_n); [ queue | refine_let (rev (snd r_n)); queue | queue ] | queue | ]. cleanup; done. finalize. Defined.
imports: Tutorial