Changed the proof of list_of_length_b_implies_element_at_b into something more vague. Still can't prove it though.