instDecidableLeThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂)
instDecidableLeThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂)