proposition: Lemma cycle_shift_shift n phi : bounded n phi -> phi[cycle_shift n] = phi[↑].
proof: Proof. intros H. apply (bounded_subst H). intros k. unfold cycle_shift. decide _; trivial; lia. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia