cases v
j : ℕ
zs : List String
v : Var
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ v.freeVarSet ∪ (List.map free_ zs).toFinset
case free_
j : ℕ
zs : List String
a✝ : String
⊢ (Var.openList j (List.map free_ zs) (free_ a✝)).freeVarSet ⊆ (free_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case bound_
j : ℕ
zs : List String
a✝ : ℕ
⊢ (Var.openList j (List.map free_ zs) (bound_ a✝)).freeVarSet ⊆ (bound_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset