case _ c1 =>
  have s1 : i < j
  linarith
  simp only [if_pos s1]
  simp only [shift]
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
no goals