simp only [Holds]
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
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
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V (hd :: tl) (def_ X xs) ↔ Holds D I V (hd :: tl) (def_ X xs)
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
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
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D (I' D I V' (hd :: tl) P zs H) V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)