{J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} →
        {e : J} →
          {motive : D.IsTerminal e → Sort u} →
            (t : D.IsTerminal e) →
              ((prop_id : D.W (CategoryTheory.CategoryStruct.id e)) →
                  (lift : {j : J} → D.P j → (j ⟶ e)) →
                    (hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)) →
                      (uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ) →
                        (comm :
                            ∀ {i j : J} (f : i ⟶ j) (hf : D.W f),
                              CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯) →
                          motive { prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm }) →
                motive t