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

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

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

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