∀ {m : Type w → Type w'} {α : Type w} {Property : α → Prop} {operation : m (Subtype Property)} {Property_1 : α → Prop}
  {operation_1 : m (Subtype Property_1)},
  { Property := Property, operation := operation } = { Property := Property_1, operation := operation_1 } →
    Property = Property_1 ∧ operation ≍ operation_1