simp only [predVarSet] 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
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs