{α : Type u_1} →
  (le lt : α → α → Prop) →
    (le_refl : ∀ (a : α), le a a) →
      (le_trans : ∀ (a b c : α), le a b → le b c → le a c) →
        (lt_iff_le_not_ge : autoParam (∀ (a b : α), lt a b ↔ le a b ∧ ¬le b a) Preorder.lt_iff_le_not_ge._autoParam) →
          (le_antisymm : ∀ (a b : α), le a b → le b a → a = b) →
            (sup : α → α → α) →
              (le_sup_left : ∀ (a b : α), le a (sup a b)) →
                (le_sup_right : ∀ (a b : α), le b (sup a b)) →
                  (sup_le : ∀ (a b c : α), le a c → le b c → le (sup a b) c) →
                    (inf : α → α → α) →
                      (inf_le_left : ∀ (a b : α), le (inf a b) a) →
                        (inf_le_right : ∀ (a b : α), le (inf a b) b) →
                          (le_inf : ∀ (a b c : α), le a b → le a c → le a (inf b c)) →
                            (sSup : Set α → α) →
                              (∀ (s : Set α), ∀ a ∈ s, le a (sSup s)) →
                                (∀ (s : Set α) (a : α), (∀ b ∈ s, le b a) → le (sSup s) a) →
                                  (sInf : Set α → α) →
                                    (∀ (s : Set α), ∀ a ∈ s, le (sInf s) a) →
                                      (∀ (s : Set α) (a : α), (∀ b ∈ s, le a b) → le a (sInf s)) →
                                        (top : α) →
                                          (∀ (a : α), le a top) →
                                            (bot : α) →
                                              (∀ (a : α), le bot a) →
                                                (∀ (x y z : α), le ((x ⊔ y) ⊓ (x ⊔ z)) (x ⊔ y ⊓ z)) →
                                                  (compl : α → α) →
                                                    (sdiff himp : α → α → α) →
                                                      (∀ (x : α), le (x ⊓ compl x) bot) →
                                                        (∀ (x : α), le top (x ⊔ compl x)) →
                                                          autoParam (∀ (x y : α), sdiff x y = x ⊓ compl y)
                                                              BooleanAlgebra.sdiff_eq._autoParam →
                                                            autoParam (∀ (x y : α), himp x y = y ⊔ compl x)
                                                                BooleanAlgebra.himp_eq._autoParam →
                                                              CompleteBooleanAlgebra α