case pred_occurs_in h1_X h1_ts h1_1 h1_2 =>
  obtain s1 := Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id zs h1_ts) H h1_2
  obtain s2 := Function.updateListITE_comp id V zs h1_ts
  simp only [s2] at s1
  simp at s1
  specialize h2 h1_X (List.map V h1_ts)
  simp only [s1] at h2
  simp only [Holds]
  apply h2
  simp
  exact h1_1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
no goals