{R : Type u_4} →
  {S : Type u_5} →
    {inst : CommRing R} →
      {inst_1 : CommRing S} →
        {inst_2 : Algebra R S} →
          {P : Sort u} →
            {P_1 : StandardEtalePair R} →
              {x : S} →
                {hasMap : P_1.HasMap x} →
                  {lift_bijective : Function.Bijective ⇑(P_1.lift x hasMap)} →
                    {P' : StandardEtalePair R} →
                      {x' : S} →
                        {hasMap' : P'.HasMap x'} →
                          {lift_bijective' : Function.Bijective ⇑(P'.lift x' hasMap')} →
                            { P := P_1, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
                                { P := P', x := x', hasMap := hasMap', lift_bijective := lift_bijective' } →
                              (P_1 ≍ P' → x ≍ x' → P) → P