cases h1_right
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right : (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
left✝ : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
right✝ : xs.length = (τ X xs.length).1.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))