case pos c1 c2 =>
  simp
  simp only [Var.freeVarSet]
  simp
  apply List.get_mem
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (List.map free_ zs)[i - j].freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
no goals