{X : AlgebraicGeometry.Scheme} →
  {motive : X.IsQuasiAffine → Sort u_1} →
    ([toCompactSpace : CompactSpace ↥X] → [toIsImmersion : AlgebraicGeometry.IsImmersion X.toSpecΓ] → motive ⋯) →
      (t : X.IsQuasiAffine) → motive t