proposition: Lemma soundness' {ff : falsity_flag} phi : [] ⊢I phi -> valid phi.
proof: Proof. intros H % soundness. intros D I rho. now apply H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Deduction.FragmentND Undecidability(Shared.ListAutomation) Vector Lia