simp only [sub] at 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 V tl (sub τ (def_ X xs)) ↔
    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 }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    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 }
      V tl (def_ X xs)
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 V tl (def_ X xs) ↔
    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 }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    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 }
      V tl (def_ X xs)