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