proposition: Lemma valid_atom_subst_compat phi : valid phi -> valid phi [s/atom].
proof: Proof. Proof using Hresp. intros H D I rho. unshelve apply <- sat_atom_subst_compat. 1:exact 0. apply H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia