   \\ fs [flatSemTheory.do_app_def,list_case_eq,CaseEq "flatSem$v",PULL_EXISTS,          CaseEq "ast$lit",store_assign_def,option_case_eq,CaseEq "store_v"]   \\ rw [] \\ fs [] \\ rveq \\ fs [LENGTH_EQ_NUM_compute] \\ rveq \\ fs []   \\ rpt (qpat_x_assum `v_rel _ _` mp_tac)   \\ once_rewrite_tac [v_rel_cases] \\ fs []   \\ rpt strip_tac \\ rveq \\ fs [do_word_op_def]   \\ rveq \\ fs [compile_op_def,arg0_def]   \\ fs [] \\ rveq \\ fs [PULL_EXISTS,SWAP_REVERSE_SYM,v_rel_def] \\ rveq \\ fs []   \\ simp [evaluate_def,do_app_def