proposition: Theorem more_automated_implementation : FullySharpened spec.
proof: Proof. start sharpening ADT. hone representation using absRel. monad_simpl. pick. done. monad_simpl. pick. done. refine_testnil (fst r_n). refine_testnil (snd r_n). assert (r_o = nil) by eauto. subst. monad_simpl. pick. monad_simpl. done. refine_let (rev (snd r_n)). erewrite eta_abs_snd with (abs := r_o) by eauto. monad_simpl. pick. monad_simpl. erewrite absRel_reversed_data by eauto. done. cbv beta. done. erewrite eta_abs_fst with (abs := r_o) by eauto. monad_simpl. pick. monad_simpl. erewrite absRel_fast_data with (abs := r_o) by eauto. done. cleanup. done. finalize. Defined.
imports: Tutorial