proposition: Corollary tsoundness_class {ff : falsity_flag} T phi : T ⊢TC phi -> forall D (I : interp D) rho, (forall psi, T psi -> rho ⊨ psi) -> rho ⊨ phi.
proof: Proof. Proof using LEM. intros (A & H1 & H2) D I rho HI. apply (soundness_class H2). intros psi HP. apply HI, H1, HP. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullND Undecidability(Shared.ListAutomation) Vector Lia