apply h1_1
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ False
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = zs.length