simp only [I']
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_