 \\ fs [])   THEN0    (imp_res_tac lookup_array \\ fs [GREATER_EQ,GSYM NOT_LESS,v_rel_def]     \\ fs [bool_case_eq] \\ rveq \\ fs [integerTheory.int_le]     \\ fs [v_rel_def]     \\ imp_res_tac LIST_REL_LENGTH     \\ fs [PULL_EXISTS]     \\ rename [`i0 < _:int`]     \\ 