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