case pred_var_ X xs =>
  simp only [predVarSet] at h1
  simp at h1
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
no goals