Cleaned up the proof of element_at_index_cons a little.