∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
  [IsNonstrictStrictOrder α (fun x1 x2 => x1 ⊆ x2) fun x1 x2 => x1 ⊂ x2] {a b : α} [Std.Antisymm fun x1 x2 => x1 ⊆ x2],
  a ⊆ b → ¬a ⊂ b → a = b