∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁) (inst unfold : Lean.Expr),
  sizeOf { e := e, src := src, tgt := tgt, inst := inst, unfold := unfold } =
    1 + sizeOf e + sizeOf src + sizeOf tgt + sizeOf inst + sizeOf unfold