proposition: Lemma m_decidable m : (forall p, decidable (fun v => i_atom (interp := model_interp m) (P:=p) v)).
proof: Proof. intros [ ]. exists (@decider_of_annoying_type m). intros v. unfold decider_of_annoying_type. cbn. destruct (proj_vec2 ) as [l r]. destruct (@rel_decider m l r) as [Ht|Hf] eqn:Heq. * unfold reflects; tauto. * unfold reflects. split. 1:intros k;exfalso;apply Hf;easy. intros Hc. congruence. 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