fact: Definition rbig_flat (n : count) (var : Type) := Eval cbv beta in ltac:(let v := (eval lazy [big_flat] in (big_flat 1 n)) in let rv := ParametricityCommon.reify var v in exact rv).
imports: Coq.Lists.List Coq.NArith.NArith PerformanceExperiments.Sandbox Reify.ReifyCommon Reify.PHOASUtil Reify.BenchmarkUtil