proposition: Lemma remove_emplace_exists r frm n : r ⊨ emplace_exists n frm -> exists rr, rr ⊨ frm /\ forall k, r k = rr (k+n).
proof: Proof. unfold emplace_exists. intros H. induction n as [|n IH] in H,frm|-*. - exists r. split. 1:easy. intros k. now rewrite Nat.add_0_r. - rewrite it_shift in H. destruct (IH _ H) as [rr [[d Hd] Hrrr]]. exists (d .: rr). split. 1:easy. intros k. rewrite Nat.add_succ_r. cbn. now apply Hrrr. 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