apply ih
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
no goals