case nil =>
  simp only [Holds]
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
no goals