simp at h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    if xs.length = ((τ X xs.length).get ⋯).1.length then
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
    else True
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))