simp only [hd.h2]
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)