finish updating compile_val proof with new hypothesis

about existence of primitive fromList code