{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f g : a ⟶ b} →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
            {η : f ⟶ g} →
              {motive : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η → Sort u_1} →
                ((lift :
                      Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f ⟶
                        Mathlib.Tactic.BicategoryCoherence.LiftHom.lift g) →
                    motive { lift := lift }) →
                  (t : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η) → motive t