case pred_ X vs =>
  simp only [Holds]
  congr! 1
  simp
D : Type
I : Interpretation D
zs : List String
X : String
vs : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ X vs) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ X vs))
no goals