case eq_ x y =>
  simp only [isFreeIn] at h1
  simp only [subAux]
  simp only [Holds]
  have s1 : V' x = V (σ x)
  apply h1
  simp
  simp only [s1]
  have s2 : V' y = V (σ y)
  apply h1
  simp
  simp only [s2]
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), isFreeIn x_1 (eq_ x y) → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (subAux c τ σ (eq_ x y))
no goals