Proved a variation of list_of_length_b_implies_element_at_b, and adjusted insert_leaf_works to work with it.