[STATEMENT]
lemma fst_annotate_rlen_le: "(k, a) \<in> set (annotate_rlen l) \<Longrightarrow> k < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, a) \<in> set (annotate_rlen l) \<Longrightarrow> k < length l
[PROOF STEP]
by(induction l arbitrary: k; simp; force)