(motive : Mathlib.Tactic.BicategoryLike.StructuralAtom → Sort u_1) →
  (η : Mathlib.Tactic.BicategoryLike.StructuralAtom) →
    ((α : Mathlib.Tactic.BicategoryLike.CoherenceHom) →
        motive (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α)) →
      ((e : Lean.Expr) →
          (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) →
            motive (Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e f g h)) →
        ((e : Lean.Expr) →
            (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
              motive (Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f)) →
          ((e : Lean.Expr) →
              (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
                motive (Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f)) →
            ((e : Lean.Expr) →
                (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
                  motive (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f)) →
              motive η