proposition: Fact TM_sat (rho : nat -> unit) (phi : form falsity_off) : rho ⊨ phi.
proof: Proof. revert rho. remember falsity_off as ff. induction phi; cbn; trivial. - discriminate. - destruct b0; auto. - destruct q; firstorder. exact tt. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia