proposition: Lemma m_P' m (e : env (model m)) (a : nat) : e ⊨ P' a <-> exists nl ul nr ur, (e a) = Pair (@fN _ nl ul) (@fN _ nr ur).
proof: Proof. split. - cbn -[model_rel]. destruct (e a) as [[n1 u1]|[nl ul] [nr ur]]. + intros H. exfalso. unfold model_rel in H. apply H. lia. + unfold model_rel. intros H. exists nl, ul, nr, ur. easy. - intros [nl [ul [nr [ur Heq]]]]. cbn. rewrite Heq. lia. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions