induction F
z : String
t : Var
F : Formula
⊢ (Formula.subst (free_ z) t F).freeVarSet ⊆ t.freeVarSet ∪ F.freeVarSet \ {free_ z}
case pred_
z : String
t : Var
a✝¹ : String
a✝ : List Var
⊢ (Formula.subst (free_ z) t (pred_ a✝¹ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ a✝¹ a✝).freeVarSet \ {free_ z}

case not_
z : String
t : Var
a✝ : Formula
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t a✝.not_).freeVarSet ⊆ t.freeVarSet ∪ a✝.not_.freeVarSet \ {free_ z}

case imp_
z : String
t : Var
a✝¹ a✝ : Formula
a_ih✝¹ : (Formula.subst (free_ z) t a✝¹).freeVarSet ⊆ t.freeVarSet ∪ a✝¹.freeVarSet \ {free_ z}
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (a✝¹.imp_ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (a✝¹.imp_ a✝).freeVarSet \ {free_ z}

case forall_
z : String
t : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (forall_ a✝¹ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ a✝¹ a✝).freeVarSet \ {free_ z}