∀ {level₂ level₁ level₀ : Lean.Level} {B : Q(Type level₀)} {instBicategory : Q(CategoryTheory.Bicategory «$B»)}
  {level₂_1 level₁_1 level₀_1 : Lean.Level} {B_1 : Q(Type level₀_1)}
  {instBicategory_1 : Q(CategoryTheory.Bicategory «$B_1»)},
  { level₂ := level₂, level₁ := level₁, level₀ := level₀, B := B, instBicategory := instBicategory } =
      { level₂ := level₂_1, level₁ := level₁_1, level₀ := level₀_1, B := B_1, instBicategory := instBicategory_1 } →
    level₂ = level₂_1 ∧ level₁ = level₁_1 ∧ level₀ = level₀_1 ∧ B = B_1 ∧ instBicategory = instBicategory_1