simp only [Holds]
D : Type
I : Interpretation D
M : MetaValuation D
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I V' M [] (def_ X xs)
no goals