proposition: Lemma cycle_shift_subject n phi : bounded (S n) phi -> phi[$n..][cycle_shift n] = phi.
proof: Proof. intros H. erewrite subst_comp, (bounded_subst H), subst_id; trivial. intros []; cbn; unfold cycle_shift; destruct (Dec _); trivial; lia. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts