proposition: Lemma FST_model : exists V (M : interp V), extensional M /\ @standard _ M /\ forall rho, rho ⊫ FST.
proof: Proof. exists hfs, hfs_interp. split; try reflexivity. split; try apply hfs_model. intros x Hx. destruct (hfs_model_standard Hx) as [n Hn]. now exists n. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts FST) Undecidability.FOL(Sets.FST) Undecidability.FOL.TRAKHTENBROT(hfs) Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability(Shared.ListAutomation) Coq(Lia)