proposition: Lemma IB_emplace_forall rho n i : (forall f, (fun k => if k <? n then f (k) else rho (k-n)) ⊨ i) -> rho ⊨ emplace_forall n i.
proof: Proof. intros H. induction n as [|n IH] in rho,H|-*. - cbn. eapply (sat_ext IB (rho := rho) (xi:=fun k => rho(k-0))). 2: apply (H (fun _ => Num 0)). intros x. now rewrite Nat.sub_0_r. - intros d. specialize (IH (d.:rho)). apply IH. intros f. eapply (sat_ext IB (xi:=fun k => if k <? S n then (fun kk => if kk =? n then d else f kk) k else (rho) (k - S n))). 2: eapply H. intros x. destruct (Nat.eq_dec x n) as [Hxn|Hnxn]. + destruct (Nat.ltb_ge x n) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. destruct (Nat.ltb_lt x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. cbn. assert (x-n=0) as ->. 1: lia. cbn. destruct (Nat.eqb_eq x n) as [_ HH]. now rewrite HH. + destruct (x <? n) eqn:Hneq. * destruct (Nat.ltb_lt x n) as [Hlt _]. apply Hlt in Hneq. clear Hlt. destruct (Nat.ltb_lt x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. cbn. destruct (Nat.eqb_neq x n) as [_ HH]. rewrite HH. 1: easy. lia. * destruct (Nat.ltb_ge x n) as [Hlt _]. apply Hlt in Hneq. clear Hlt. destruct (Nat.ltb_ge x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. assert (x-n=S(x-S n)) as ->. 1:lia. easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Utils.FriedmanTranslationFragment 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) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_constructions)