{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l : Mathlib.Tactic.FieldSimp.qNF M) →
        Lean.MetaM
          ((e : Q(«$M»)) ×
            let a := l.toNF;
            let foldr_1 :=
              List.foldr
                (fun x l =>
                  match x with
                  | ((a, x), snd) => q((«$a», «$x») ::ᵣ «$l»))
                q([]) l;
            Q(«$foldr_1».eval = «$e»))