proposition: Lemma mDN_sat rho phi : mDN (rho ⊨ phi) -> rho ⊨ phi.
proof: Proof. induction phi as [| |?[]|?[]] in rho|-*; cbn -[dom_rel']; intros H. - apply H. tauto. - intros Hc. apply H. intros Hc2. now apply Hc2. - intros H1. apply IHphi2. intros Hc. apply H. intros Hv. apply Hc, Hv, H1. - intros d. apply IHphi. intros Hc. apply H. intros Hc2. apply Hc, Hc2. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Utils.FriedmanTranslationFragment Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_constructions)