simp only [Holds]
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
V : Valuation D
d : D
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
no goals