case nil =>
  simp only [Holds] at h1
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length
no goals