Draft: test_to_list_of_list_proof

I think I need to use of_list_is_valid for this proof but I am unsure how I should provide the arguments.

The current state of the proof is shown: