proposition: Fact iter_switch {X} f n x : f (@iter X f n x) = iter f n (f x).
proof: Proof. induction n; cbn; now try rewrite IHn. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)