verify (and fix) the bytecode implementing fromList

adds an assumption to the prim1_to_bc_thm saying that the code must
contain the primitives (in this case only one primitive, for fromList)
at the expected labels. this assumption will probably carry throughout
this file and need to be satisfied higher up when the initial bytecode
state is created.