simp only [Interpretation.usingPred]
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 ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (Interpretation.usingPred D I 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) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds).pred_const_
      X (List.map V' xs) ↔
    I.pred_const_ X (List.map V (List.map σ xs))
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 ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ I.pred_const_ X (List.map V' xs) ↔ I.pred_const_ X (List.map V (List.map σ xs))