split_ifs
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V' xs)
    else I.pred_var_ X (List.map V' xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
            ((τ X xs.length).get ⋯).2
        else pred_var_ X (List.map σ xs)
      else pred_var_ X (List.map σ xs))
case pos
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝¹ : (τ X xs.length).isSome = true
h✝ : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V'' ((τ X xs.length).get ⋯).1 (List.map V' xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 (List.map σ xs)) c
        ((τ X xs.length).get ⋯).2)

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝¹ : (τ X xs.length).isSome = true
h✝ : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))

case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
h✝ : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))