[STATEMENT]
lemma vec_comp_allE:
  "vec_comp_all r v w \<Longrightarrow> i < dim_vec v \<Longrightarrow> r (v $ i) (w $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vec_comp_all r v w; i < dim_vec v\<rbrakk> \<Longrightarrow> r (v $ i) (w $ i)
[PROOF STEP]
unfolding vec_comp_all_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<dim_vec v. r (v $ i) (w $ i); i < dim_vec v\<rbrakk> \<Longrightarrow> r (v $ i) (w $ i)
[PROOF STEP]
by auto