proposition: Lemma specialize_list (H f:form) (l:list nat) (n:nat) : length l = n -> (H[subst_list l >> var]:: nil) ⊢I f -> (emplace_forall n H::nil) ⊢I f.
proof: Proof. induction l as [|lx lr IH] in n,H|-*. - intros <-. cbn. now erewrite subst_id. - intros <- Hpr. cbn [length]. specialize (IH (∀ H) (length lr) eq_refl). cbn in IH. rewrite emplace_forall_shift in IH. eapply IH, IE. + apply Weak with nil. 2:easy. apply II, Hpr. + assert (H[up (subst_list lr >> var)][$lx..] = H[subst_list (lx :: lr) >> var]) as <-. * rewrite subst_comp. apply subst_ext. now intros [|n]. * apply AllE, Ctx. now left. 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)