[STATEMENT]
lemma ROI_init:
  assumes "CNV_ANNOT a a' R"
  assumes "(c,a')\<in>R"
  shows "(c,a)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, a) \<in> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CNV_ANNOT a a' R
(c, a') \<in> R

goal (1 subgoal):
 1. (c, a) \<in> R
[PROOF STEP]
by simp