case bound_ i =>
  simp only [Var.open]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
j : ℕ
z : String
i : ℕ
⊢ (Var.open j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}
no goals