{α : Type u_1} →
  {motive : CompleteDistribLattice α → Sort u} →
    ([toFrame : Order.Frame α] →
        [toSDiff : SDiff α] →
          (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) →
            [toHNot : HNot α] →
              (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) →
                motive
                  { toFrame := toFrame, toSDiff := toSDiff, sdiff_le_iff := sdiff_le_iff, toHNot := toHNot,
                    top_sdiff := top_sdiff }) →
      (t : CompleteDistribLattice α) → motive t