Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
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
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      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
    else
      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 }
        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)
Tactic:
split_ifs
Proof state after:
case pos
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
h✝ : 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 neg
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
h✝ : ¬(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 }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)