cases v
j : ℕ
z : String
v : Var
⊢ (Var.close j (free_ z) v).freeVarSet ⊆ v.freeVarSet \ {free_ z}
case free_
j : ℕ
z a✝ : String
⊢ (Var.close j (free_ z) (free_ a✝)).freeVarSet ⊆ (free_ a✝).freeVarSet \ {free_ z}

case bound_
j : ℕ
z : String
a✝ : ℕ
⊢ (Var.close j (free_ z) (bound_ a✝)).freeVarSet ⊆ (bound_ a✝).freeVarSet \ {free_ z}