case nil =>
  simp only [Holds]
D : Type
I : Interpretation D
V'' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (def_ X xs) → V' x = V (σ x)
h2 : ∀ x ∈ (def_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' [] τ) V' [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
no goals