∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A B X : C}
  {P : HomotopicalAlgebra.PathObject B} {f₀ f₁ : A ⟶ B} [HomotopicalAlgebra.IsFibrant B] [P.IsGood]
  (h : P.RightHomotopy f₀ f₁) (i : A ⟶ X) [HomotopicalAlgebra.Cofibration i] (l₀ : X ⟶ B),
  autoParam (CategoryTheory.CategoryStruct.comp i l₀ = f₀)
      HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension._auto_1 →
    ∃ l₁ h', CategoryTheory.CategoryStruct.comp i h'.h = h.h