rw [←hl] at hj h'
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
h' : i < j
hi : i < List.length (a₁ :: a₂ :: as)
hj : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]