simp only [Holds]
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
no goals