[STATEMENT]
lemma rb_aux_inv1_D5:
  "rb_aux_inv1 bs \<Longrightarrow> i < length bs \<Longrightarrow> is_RB_upt dgrad rword (set (drop (Suc i) bs)) (lt (bs ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rb_aux_inv1 bs; i < length bs\<rbrakk> \<Longrightarrow> is_RB_upt dgrad rword (set (drop (Suc i) bs)) (lt (bs ! i))
[PROOF STEP]
by (simp add: rb_aux_inv1_def)