∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (motive : f.Homotopy g → Prop) (h : f.Homotopy g),
  (∀ (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj (SimplexCategory.mk 1)) ⟶ Y)
      (h₀ :
        autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam)
      (h₁ :
        autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam)
      (rel :
        autoParam
          (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj (SimplexCategory.mk 1))) h =
            CategoryTheory.CategoryStruct.comp
              (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj (SimplexCategory.mk 1)))
              (CategoryTheory.CategoryStruct.comp φ B.ι))
          SSet.RelativeMorphism.Homotopy.rel._autoParam),
      motive { h := h, h₀ := h₀, h₁ := h₁, rel := rel }) →
    motive h