proposition: Lemma proj_vec2_correct D x y v : proj_vec2 v = (x,y) <-> v = Vector.cons D x 1 (Vector.cons D y 0 (Vector.nil D)).
proof: Proof. split. - refine (match v with @Vector.nil _ => _ | @Vector.cons _ x' n xr => _ end). 1:easy. destruct n as [|[|n]]. 1,3:easy. refine (match xr with @Vector.nil _ => _ | @Vector.cons _ y' n yr => _ end). 1:easy. destruct n as [|n]. 2:easy. cbn. intros H. f_equal. 2:f_equal. 1-2:congruence. refine (match yr with @Vector.nil _ => _ end). easy. - intros ->. easy. 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