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