case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) F
⊢ shift D V d (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ i) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ i))
no goals