rcases hor with (heq | hmem)
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a
case mpr.nil.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
heq : x = a
⊢ x = a

case mpr.nil.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hmem : x ∈ []
⊢ x = a