∀ (α : Type u_2) [semilatticeInf : SemilatticeInf α] [orderBot : OrderBot α] [predOrder : PredOrder α]
  [isPredArchimedean : IsPredArchimedean α] (α_1 : Type u_2) (semilatticeInf_1 : SemilatticeInf α_1)
  (orderBot_1 : OrderBot α_1) (predOrder_1 : PredOrder α_1) (isPredArchimedean_1 : IsPredArchimedean α_1),
  ({ α := α, semilatticeInf := semilatticeInf, orderBot := orderBot, predOrder := predOrder,
        isPredArchimedean := isPredArchimedean } =
      { α := α_1, semilatticeInf := semilatticeInf_1, orderBot := orderBot_1, predOrder := predOrder_1,
        isPredArchimedean := isPredArchimedean_1 }) =
    (α = α_1 ∧ semilatticeInf ≍ semilatticeInf_1 ∧ orderBot ≍ orderBot_1 ∧ predOrder ≍ predOrder_1)