-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.NormalizedHom →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr) →
    (Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr) →
      (Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.NormalizedHom →
            Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr) →
        (Mathlib.Tactic.BicategoryLike.NormalizedHom →
            Mathlib.Tactic.BicategoryLike.NormalizedHom →
              Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr) →
          (Mathlib.Tactic.BicategoryLike.NormalizedHom →
              Mathlib.Tactic.BicategoryLike.NormalizedHom →
                Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₁ →
                    Mathlib.Tactic.BicategoryLike.Mor₁ →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                        Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                          Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr) →
            (Mathlib.Tactic.BicategoryLike.NormalizedHom →
                Mathlib.Tactic.BicategoryLike.NormalizedHom →
                  Mathlib.Tactic.BicategoryLike.NormalizedHom →
                    Mathlib.Tactic.BicategoryLike.Mor₁ →
                      Mathlib.Tactic.BicategoryLike.Mor₁ →
                        Mathlib.Tactic.BicategoryLike.Mor₁ →
                          Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                              Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr) →
              (Mathlib.Tactic.BicategoryLike.NormalizedHom →
                  Mathlib.Tactic.BicategoryLike.NormalizedHom →
                    Mathlib.Tactic.BicategoryLike.NormalizedHom →
                      Mathlib.Tactic.BicategoryLike.Mor₁ →
                        Mathlib.Tactic.BicategoryLike.Mor₁ →
                          Mathlib.Tactic.BicategoryLike.Mor₁ →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                              Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                  Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr) →
                (Mathlib.Tactic.BicategoryLike.NormalizedHom →
                    Mathlib.Tactic.BicategoryLike.NormalizedHom →
                      Mathlib.Tactic.BicategoryLike.NormalizedHom →
                        Mathlib.Tactic.BicategoryLike.Mor₁ →
                          Mathlib.Tactic.BicategoryLike.Mor₁ →
                            Mathlib.Tactic.BicategoryLike.Mor₁ →
                              Mathlib.Tactic.BicategoryLike.Mor₁ →
                                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                      Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                        Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                          Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr) →
                  (Mathlib.Tactic.BicategoryLike.NormalizedHom →
                      Mathlib.Tactic.BicategoryLike.NormalizedHom →
                        Mathlib.Tactic.BicategoryLike.Mor₁ →
                          Mathlib.Tactic.BicategoryLike.Mor₁ →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                              Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                                Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr) →
                    Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m