simp only [Formula.Forall_]
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (Forall_ xs P) ↔ x ∈ xs ∨ isBoundIn x P
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (List.foldr forall_ P xs) ↔ x ∈ xs ∨ isBoundIn x P