simp only [Holds]
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_
no goals