have s1 :
  Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H :=
  by
  apply Holds_coincide_Var
  intro v a1
  apply Function.updateListITE_updateIte
  intro contra
  subst contra
  contradiction
case h.h2
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 : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (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 h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
case h.h2
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 : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (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 h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 :
  Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds