apply IsSub.pred_var_
v u : VarName
X : PredName
xs : List VarName
binders : Finset VarName
h1 : v ∈ xs → u ∉ binders
⊢ IsSub (pred_var_ X xs) v u (pred_var_ X (List.map (fun x => if v = x then u else x) xs))
no goals