no goals
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : reverse l₁ <:+ reverse l₂
r : List α✝
e : r ++ reverse l₁ = reverse l₂
⊢ l₁ ++ reverse r = l₂
rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]
no goals
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <+: l₂
r : List α✝
e : l₁ ++ r = l₂
⊢ reverse r ++ reverse l₁ = reverse l₂
rw [← reverse_append, e]