{α : Type u_2} →
  [inst : BooleanAlgebra α] →
    {motive : BooleanSubalgebra α → Sort u} →
      ((toSublattice : Sublattice α) →
          (compl_mem' : ∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier) →
            (bot_mem' : ⊥ ∈ toSublattice.carrier) →
              motive { toSublattice := toSublattice, compl_mem' := compl_mem', bot_mem' := bot_mem' }) →
        (t : BooleanSubalgebra α) → motive t