α✝ : Type u_1
l₁ l₂ : List α✝
⊢ reverse (reverse l₁) <:+ reverse (reverse l₂) ↔ l₁ <:+ l₂
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂
rw [← reverse_suffix]
no goals
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ reverse (reverse l₁) <:+ reverse (reverse l₂) ↔ l₁ <:+ l₂
simp only [reverse_reverse]