proposition: Lemma insert_S_S {X : Type} n i (f : nat -> X) x : insert (S i) f x (S n) = insert i (fun n => f (S n)) x n.
proof: Proof. unfold insert. destruct (Compare_dec.lt_eq_lt_dec _ _) as [[|]|]; destruct (Compare_dec.lt_eq_lt_dec _ _) as [[|]|]. all: destruct n as [|?]; trivial; lia. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec