simp only [Holds]
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (eq_ x y) ↔ Holds D I (Function.updateITE V v d) M E (eq_ x y)
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y