proposition: Lemma emplace_forall_subst (n:nat) (i:form) sigma : (emplace_forall n i)[sigma] = emplace_forall n (i[it up n sigma]).
proof: Proof. induction n as [|n IH] in sigma|-*. - easy. - cbn. f_equal. now rewrite IH, <- it_shift. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)