simp only [Holds]
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E false_ ↔ Holds D I V' E false_
no goals