proposition: Lemma sshift_spec {Σ_funcs : funcs_signature} k n : @sshift' Σ_funcs k n = sshift k n.
proof: Proof. induction k as [|k IH] in n|-*. - easy. - destruct n as [|n]. + easy. + cbn. specialize (IH (S (S n))). cbn in IH. rewrite <- plus_n_Sm in IH. rewrite IH. easy. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Asimpl Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets(binZF ZF) Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation) Morphisms