∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S]
  (f : X.PartialMap Y), AlgebraicGeometry.Scheme.PartialMap.IsOver S f = AlgebraicGeometry.Scheme.Hom.IsOver f.hom S