induction F generalizing σ
σ : VarName → VarName
c : Char
F : Formula
⊢ (sub σ c F).freeVarSet = Finset.image σ F.freeVarSet
case pred_const_
c : Char
a✝¹ : PredName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (pred_const_ a✝¹ a✝)).freeVarSet = Finset.image σ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
c : Char
a✝¹ : PredName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (pred_var_ a✝¹ a✝)).freeVarSet = Finset.image σ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
c : Char
a✝¹ a✝ : VarName
σ : VarName → VarName
⊢ (sub σ c (eq_ a✝¹ a✝)).freeVarSet = Finset.image σ (eq_ a✝¹ a✝).freeVarSet

case true_
c : Char
σ : VarName → VarName
⊢ (sub σ c true_).freeVarSet = Finset.image σ true_.freeVarSet

case false_
c : Char
σ : VarName → VarName
⊢ (sub σ c false_).freeVarSet = Finset.image σ false_.freeVarSet

case not_
c : Char
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c a✝.not_).freeVarSet = Finset.image σ a✝.not_.freeVarSet

case imp_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.imp_ a✝)).freeVarSet = Finset.image σ (a✝¹.imp_ a✝).freeVarSet

case and_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.and_ a✝)).freeVarSet = Finset.image σ (a✝¹.and_ a✝).freeVarSet

case or_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.or_ a✝)).freeVarSet = Finset.image σ (a✝¹.or_ a✝).freeVarSet

case iff_
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (σ : VarName → VarName), (sub σ c a✝¹).freeVarSet = Finset.image σ a✝¹.freeVarSet
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (a✝¹.iff_ a✝)).freeVarSet = Finset.image σ (a✝¹.iff_ a✝).freeVarSet

case forall_
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (forall_ a✝¹ a✝)).freeVarSet = Finset.image σ (forall_ a✝¹ a✝).freeVarSet

case exists_
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (σ : VarName → VarName), (sub σ c a✝).freeVarSet = Finset.image σ a✝.freeVarSet
σ : VarName → VarName
⊢ (sub σ c (exists_ a✝¹ a✝)).freeVarSet = Finset.image σ (exists_ a✝¹ a✝).freeVarSet

case def_
c : Char
a✝¹ : DefName
a✝ : List VarName
σ : VarName → VarName
⊢ (sub σ c (def_ a✝¹ a✝)).freeVarSet = Finset.image σ (def_ a✝¹ a✝).freeVarSet