fact: Definition forall_times {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia