case _ x' =>
  simp only [shift]
  simp only [Var.openList]
  split_ifs
  case _ c1 =>
    simp at c1
    simp only [← c1] at h1
    contradiction
  case _ c1 =>
    rfl
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ shift D V d (free_ x') =
    if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
no goals