case inl
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a : Fin (length l)
hab : a ≤ a
⊢ r (get l a) (get l a)

case inr
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin (length l)
hab : a ≤ b
hlt : a < b
⊢ r (get l a) (get l b)
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin (length l)
hab : a ≤ b
⊢ r (get l a) (get l b)
rcases hab.eq_or_lt with (rfl | hlt)
no goals
case inl
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a : Fin (length l)
hab : a ≤ a
⊢ r (get l a) (get l a)

case inr
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin (length l)
hab : a ≤ b
hlt : a < b
⊢ r (get l a) (get l b)
exacts [refl _, h.rel_get_of_lt hlt]