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