α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ <+~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ <+~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
⊢ l₁ <+ l₂
let ⟨_, h, h'⟩ := p
no goals
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ <+~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂
rwa [← eq_of_perm_of_sorted h (s₂.sublist h') s₁]