proposition: Lemma rel_decider m (a b : model m) : dec (model_rel a b).
proof: Proof. destruct a as [[an al]|la ra], b as [[bn bl]|lb rb]. - cbn. unfold dec. destruct (leq_dec an bn); auto. - cbn. unfold dec. destruct lb; decide equality. - cbn. destruct la,ra; unfold dec. decide equality. - cbn. destruct la,ra,lb,rb. apply and_dec; unfold dec; decide equality. 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