{α : Type u} →
  {motive : BooleanAlgebra α → Sort u_1} →
    ([toDistribLattice : DistribLattice α] →
        [toCompl : Compl α] →
          [toSDiff : SDiff α] →
            [toHImp : HImp α] →
              [toTop : Top α] →
                [toBot : Bot α] →
                  (inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥) →
                    (top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ) →
                      (le_top : ∀ (a : α), a ≤ ⊤) →
                        (bot_le : ∀ (a : α), ⊥ ≤ a) →
                          (sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ) →
                            (himp_eq : ∀ (x y : α), x ⇨ y = y ⊔ xᶜ) →
                              motive
                                { toDistribLattice := toDistribLattice, toCompl := toCompl, toSDiff := toSDiff,
                                  toHImp := toHImp, toTop := toTop, toBot := toBot,
                                  inf_compl_le_bot := inf_compl_le_bot, top_le_sup_compl := top_le_sup_compl,
                                  le_top := le_top, bot_le := bot_le, sdiff_eq := sdiff_eq, himp_eq := himp_eq }) →
      (t : BooleanAlgebra α) → motive t