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

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

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

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