proposition: Lemma lift_let_list_rect T A P N C (v : A) fls : @list_rect T P N C (Let_In v fls) = Let_In v (fun v => @list_rect T P N C (fls v)).
proof: Proof. reflexivity. Qed.
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