proposition: Lemma bounded_Fr {ff : falsity_flag} N ϕ : bounded N ϕ -> bounded N (Fr ϕ).
proof: Proof. induction 1; cbn; solve_bounds; auto. - econstructor; apply H. - destruct binop; now solve_bounds. - destruct quantop; now solve_bounds. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)