apply Holds_coincide_PredVar
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      (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
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)