proposition: Theorem implementation : FullySharpened spec.
proof: Proof. start sharpening ADT. hone representation using absRel. monad_simpl. pick_by absRel_initial. done. monad_simpl. pick_by absRel_push. done. refine_testnil (fst r_n). refine_testnil (snd r_n). assert (r_o = nil) by (eapply absRel_must_be_nil; eauto). subst. monad_simpl. pick_by absRel_initial. monad_simpl. done. refine_let (rev (snd r_n)). erewrite eta_abs_snd with (abs := r_o) by eauto. monad_simpl. pick_by absRel_reversed_rep. 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_by absRel_fast_rep. monad_simpl. erewrite absRel_fast_data with (abs := r_o) by eauto. done. rewrite refine_let_ret. rewrite refine_testnil_ret. rewrite refine_testnil_ret. done. finalize. Defined.
imports: Tutorial