fact: Definition make_cps {T} (n : nat) (m : nat) (v : Z) (k : list Z -> T) := nat_rect _ (fun k => k (List.repeat v n)) (fun _ rec k => rec (fun ls => map_double_cps ls k)) m k.
imports: Coq.micromega.Lia Coq.ZArith.ZArith Coq.QArith.QArith Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Lists.List PerformanceExperiments.Harness PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances