simp only [Formula.Forall_]
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (Forall_ xs P) ↔ x ∉ xs ∧ isFreeIn x P
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P