have s1 : V' x = V (σ x)
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), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
case s1
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), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V (σ x)

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), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)