fact: Definition max_input_of_kind (k : kind_of_rewrite) : option Z := match k with | kind_rewrite_strat _ => None | kind_setoid_rewrite => None end%Z.
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