-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.HorizontalComp → m Lean.Expr) →
    (Mathlib.Tactic.BicategoryLike.WhiskerRight →
        Mathlib.Tactic.BicategoryLike.HorizontalComp →
          Mathlib.Tactic.BicategoryLike.HorizontalComp →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
      (Mathlib.Tactic.BicategoryLike.Atom₁ →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.WhiskerLeft →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
        (Mathlib.Tactic.BicategoryLike.Atom₁ →
            Mathlib.Tactic.BicategoryLike.HorizontalComp →
              Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
          (Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr) →
            (Mathlib.Tactic.BicategoryLike.Structural →
                Mathlib.Tactic.BicategoryLike.Structural →
                  Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Mathlib.Tactic.BicategoryLike.NormalExpr →
                              Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
              (Mathlib.Tactic.BicategoryLike.Structural →
                  Mathlib.Tactic.BicategoryLike.Structural →
                    Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Mathlib.Tactic.BicategoryLike.NormalExpr →
                              Mathlib.Tactic.BicategoryLike.NormalExpr →
                                Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                (Mathlib.Tactic.BicategoryLike.Structural →
                    Mathlib.Tactic.BicategoryLike.Structural →
                      Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Mathlib.Tactic.BicategoryLike.NormalExpr →
                              Mathlib.Tactic.BicategoryLike.NormalExpr →
                                Mathlib.Tactic.BicategoryLike.NormalExpr →
                                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                                      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                  Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m