{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {G : CategoryTheory.Functor C D} →
              {motive : CategoryTheory.Functor.IsDenseSubsite J K G → Sort u} →
                (t : CategoryTheory.Functor.IsDenseSubsite J K G) →
                  ((isCoverDense' : G.IsCoverDense K) →
                      (isLocallyFull' : G.IsLocallyFull K) →
                        (isLocallyFaithful' : G.IsLocallyFaithful K) →
                          (functorPushforward_mem_iff :
                              ∀ {X : C} {S : CategoryTheory.Sieve X},
                                CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X) →
                            motive ⋯) →
                    motive t