[STATEMENT]
lemma shift_inj[simp]:
"shift cl n I1 = shift cl n I2 \<longleftrightarrow> I1 = I2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.shift cl n I1 = local.shift cl n I2) = (I1 = I2)
[PROOF STEP]
unfolding shift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+) (brnL cl n) ` I1 = (+) (brnL cl n) ` I2) = (I1 = I2)
[PROOF STEP]
by force