{α : Type u_2} →
  {inst : LE α} →
    {P : Sort u} →
      {carrier : Set α} →
        {Nonempty' : carrier.Nonempty} →
          {isChain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier} →
            {carrier' : Set α} →
              {Nonempty'' : carrier'.Nonempty} →
                {isChain'' : IsChain (fun x1 x2 => x1 ≤ x2) carrier'} →
                  { carrier := carrier, Nonempty' := Nonempty', isChain' := isChain' } =
                      { carrier := carrier', Nonempty' := Nonempty'', isChain' := isChain'' } →
                    (carrier ≍ carrier' → P) → P