{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.FormallyUnramified f → Sort u_1} →
      ((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 ⋯) →
        (t : AlgebraicGeometry.FormallyUnramified f) → motive t