induction F generalizing j
j : ℕ
z : String
F : Formula
⊢ (Formula.open j (free_ z) F).freeVarSet ⊆ F.freeVarSet ∪ {free_ z}
case pred_
z a✝¹ : String
a✝ : List Var
j : ℕ
⊢ (Formula.open j (free_ z) (pred_ a✝¹ a✝)).freeVarSet ⊆ (pred_ a✝¹ a✝).freeVarSet ∪ {free_ z}

case not_
z : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.open j (free_ z) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ {free_ z}
j : ℕ
⊢ (Formula.open j (free_ z) a✝.not_).freeVarSet ⊆ a✝.not_.freeVarSet ∪ {free_ z}

case imp_
z : String
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (j : ℕ), (Formula.open j (free_ z) a✝¹).freeVarSet ⊆ a✝¹.freeVarSet ∪ {free_ z}
a_ih✝ : ∀ (j : ℕ), (Formula.open j (free_ z) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ {free_ z}
j : ℕ
⊢ (Formula.open j (free_ z) (a✝¹.imp_ a✝)).freeVarSet ⊆ (a✝¹.imp_ a✝).freeVarSet ∪ {free_ z}

case forall_
z a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.open j (free_ z) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ {free_ z}
j : ℕ
⊢ (Formula.open j (free_ z) (forall_ a✝¹ a✝)).freeVarSet ⊆ (forall_ a✝¹ a✝).freeVarSet ∪ {free_ z}