proposition: Lemma emplace_forall_elim (n:nat) (i:form) (pos:nat->nat) A : A ⊢I emplace_forall n i -> A ⊢I (i[specialize_n n pos]).
proof: Proof. intros Hpr. induction n as [|n IH] in i,pos,Hpr|-*. - cbn. now rewrite subst_id. - cbn in Hpr. enough (i[up (specialize_n n (fun l=> (pos(S l))))][$(pos 0)..] = i[specialize_n (S n) pos]) as <-. + apply AllE. specialize (IH (∀ i) (fun l => (pos (S l)))). apply IH. unfold emplace_forall. rewrite <- it_shift. cbn. apply Hpr. + rewrite subst_comp. apply subst_ext. intros [|k]. * easy. * var_cbn. rewrite subst_term_comp. var_cbn. now rewrite subst_term_id. 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)