case forall_ x phi phi_ih =>
  simp only [occursFreeIn] at h1
  simp only [Holds]
  apply forall_congr'
  intro d
  apply phi_ih
  intro v a1
  cases v
  case free_ x =>
    simp only [shift]
    apply h1
    exact a1
  case bound_ i =>
    cases i
    case zero =>
      simp only [shift]
    case succ i =>
      simp only [shift]
      apply h1
      simp only [lift]
      exact a1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ x phi) → V v = V' v
⊢ Holds D I V (forall_ x phi) ↔ Holds D I V' (forall_ x phi)
no goals