[STATEMENT]
lemma index_less_size_conv:
  "(index xs x < size xs) = (x \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index xs x < length xs) = (x \<in> set xs)
[PROOF STEP]
by(auto simp: index_def find_index_less_size_conv)