{P : Sort u} →
  {e : Lean.Expr} →
    {src tgt : Mathlib.Tactic.BicategoryLike.Mor₁} →
      {e' : Lean.Expr} →
        {src' tgt' : Mathlib.Tactic.BicategoryLike.Mor₁} →
          { e := e, src := src, tgt := tgt } = { e := e', src := src', tgt := tgt' } →
            (e = e' → src = src' → tgt = tgt' → P) → P