{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.FormallyUnramified f → Sort u_1} →
      (t : AlgebraicGeometry.FormallyUnramified f) →
        ((formallyUnramified_appLE :
              ∀ {U : Y.Opens},
                AlgebraicGeometry.IsAffineOpen U →
                  ∀ {V : X.Opens},
                    AlgebraicGeometry.IsAffineOpen V →
                      ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified) →
            motive ⋯) →
          motive t